Mathlib.Data.Set.Finite.Lattice

Set.fintypeiUnion instance

[DecidableEq α] [Fintype (PLift ι)] (f : ι → Set α) [∀ i, Fintype (f i)] : Fintype (⋃ i, f i)

Full source

instance fintypeiUnion [DecidableEq α] [Fintype (PLift ι)] (f : ι → Set α) [∀ i, Fintype (f i)] :
    Fintype (⋃ i, f i) :=
  Fintype.ofFinset (Finset.univ.biUnion fun i : PLift ι => (f i.down).toFinset) <| by simp

Finite Union of Finite Sets is Finite

Informal description

For any type $\alpha$ with decidable equality and any type $\iota$ that is finite (lifted to `PLift`), given a family of finite sets $f_i \subseteq \alpha$ indexed by $i \in \iota$, the union $\bigcup_{i \in \iota} f_i$ is also finite.

Set.fintypesUnion instance

[DecidableEq α] {s : Set (Set α)} [Fintype s] [H : ∀ t : s, Fintype (t : Set α)] : Fintype (⋃₀ s)

Full source

instance fintypesUnion [DecidableEq α] {s : Set (Set α)} [Fintype s]
    [H : ∀ t : s, Fintype (t : Set α)] : Fintype (⋃₀ s) := by
  rw [sUnion_eq_iUnion]
  exact @Set.fintypeiUnion _ _ _ _ _ H

Finite Union of Finite Sets in a Collection is Finite

Informal description

For any type $\alpha$ with decidable equality and any finite collection $s$ of subsets of $\alpha$ (where each subset in $s$ is finite), the union $\bigcup s$ is also finite.

Set.toFinset_iUnion theorem

 [Fintype β] [DecidableEq α] (f : β → Set α) [∀ w, Fintype (f w)] :
  Set.toFinset (⋃ (x : β), f x) = Finset.biUnion (Finset.univ : Finset β) (fun x => (f x).toFinset)

Full source

lemma toFinset_iUnion [Fintype β] [DecidableEq α] (f : β → Set α)
    [∀ w, Fintype (f w)] :
    Set.toFinset (⋃ (x : β), f x) =
    Finset.biUnion (Finset.univ : Finset β) (fun x => (f x).toFinset) := by
  ext v
  simp only [mem_toFinset, mem_iUnion, Finset.mem_biUnion, Finset.mem_univ, true_and]

Finset Representation of Union over Finite Index Set

Informal description

For a finite type $\beta$ and a type $\alpha$ with decidable equality, given a family of finite sets $f_w \subseteq \alpha$ indexed by $w \in \beta$, the finset corresponding to the union $\bigcup_{x \in \beta} f_x$ is equal to the finset obtained by taking the union over all $x \in \beta$ of the finsets corresponding to $f_x$. In symbols: $$\text{toFinset}\left(\bigcup_{x \in \beta} f_x\right) = \bigcup_{x \in \beta} \text{toFinset}(f_x)$$

Set.fintypeBiUnion definition

 [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s] (t : ι → Set α) (H : ∀ i ∈ s, Fintype (t i)) :
  Fintype (⋃ x ∈ s, t x)

Full source

/-- A union of sets with `Fintype` structure over a set with `Fintype` structure has a `Fintype`
structure. -/
def fintypeBiUnion [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s] (t : ι → Set α)
    (H : ∀ i ∈ s, Fintype (t i)) : Fintype (⋃ x ∈ s, t x) :=
  haveI : ∀ i : toFinset s, Fintype (t i) := fun i => H i (mem_toFinset.1 i.2)
  Fintype.ofFinset (s.toFinset.attach.biUnion fun x => (t x).toFinset) fun x => by simp

Finiteness of a union over a finite index set with finite fibers

Informal description

Given a type $\alpha$ with decidable equality, a set $s$ of type $\iota$ with a `Fintype` structure, and a family of sets $t : \iota \to \text{Set } \alpha$ such that for each $i \in s$, the set $t(i)$ has a `Fintype` structure, then the union $\bigcup_{x \in s} t(x)$ also has a `Fintype` structure.

Set.fintypeBiUnion' instance

 [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s] (t : ι → Set α) [∀ i, Fintype (t i)] : Fintype (⋃ x ∈ s, t x)

Full source

instance fintypeBiUnion' [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s] (t : ι → Set α)
    [∀ i, Fintype (t i)] : Fintype (⋃ x ∈ s, t x) :=
  Fintype.ofFinset (s.toFinset.biUnion fun x => (t x).toFinset) <| by simp

Finiteness of Union over Finite Index Set with Finite Fibers

Informal description

For any type $\alpha$ with decidable equality, a finite set $s$ of indices of type $\iota$, and a family of finite sets $t_i \subseteq \alpha$ indexed by $\iota$, the union $\bigcup_{x \in s} t_x$ is finite.

Finite.Set.finite_iUnion instance

[Finite ι] (f : ι → Set α) [∀ i, Finite (f i)] : Finite (⋃ i, f i)

Full source

instance finite_iUnion [Finite ι] (f : ι → Set α) [∀ i, Finite (f i)] : Finite (⋃ i, f i) := by
  rw [iUnion_eq_range_psigma]
  apply Set.finite_range

Finite Union of Finite Sets is Finite

Informal description

For any finite index set $\iota$ and a family of finite sets $f : \iota \to \text{Set } \alpha$, the union $\bigcup_{i \in \iota} f(i)$ is finite.

Finite.Set.finite_sUnion instance

{s : Set (Set α)} [Finite s] [H : ∀ t : s, Finite (t : Set α)] : Finite (⋃₀ s)

Full source

instance finite_sUnion {s : Set (Set α)} [Finite s] [H : ∀ t : s, Finite (t : Set α)] :
    Finite (⋃₀ s) := by
  rw [sUnion_eq_iUnion]
  exact @Finite.Set.finite_iUnion _ _ _ _ H

Finite Union of Finite Families of Sets is Finite

Informal description

For any family of sets $s$ of type $\text{Set}(\text{Set } \alpha)$ where $s$ is finite and each member of $s$ is finite, the union $\bigcup s$ is finite.

Finite.Set.finite_biUnion theorem

{ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α) (H : ∀ i ∈ s, Finite (t i)) : Finite (⋃ x ∈ s, t x)

Full source

theorem finite_biUnion {ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α)
    (H : ∀ i ∈ s, Finite (t i)) : Finite (⋃ x ∈ s, t x) := by
  rw [biUnion_eq_iUnion]
  haveI : ∀ i : s, Finite (t i) := fun i => H i i.property
  infer_instance

Finite Union of Finite Sets over a Finite Index Set

Informal description

For any type $\iota$, a finite subset $s \subseteq \iota$, and a family of sets $t : \iota \to \text{Set } \alpha$ such that $t(i)$ is finite for each $i \in s$, the union $\bigcup_{x \in s} t(x)$ is finite.

Finite.Set.finite_biUnion' instance

{ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α) [∀ i, Finite (t i)] : Finite (⋃ x ∈ s, t x)

Full source

instance finite_biUnion' {ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α) [∀ i, Finite (t i)] :
    Finite (⋃ x ∈ s, t x) :=
  finite_biUnion s t fun _ _ => inferInstance

Finite Union of Finite Sets over a Finite Index Set (Uniform Version)

Informal description

For any type $\iota$, a finite subset $s \subseteq \iota$, and a family of sets $t : \iota \to \text{Set } \alpha$ where each $t(i)$ is finite, the union $\bigcup_{x \in s} t(x)$ is finite.

Finite.Set.finite_biUnion'' instance

 {ι : Type*} (p : ι → Prop) [h : Finite {x | p x}] (t : ι → Set α) [∀ i, Finite (t i)] : Finite (⋃ (x) (_ : p x), t x)

Full source

/-- Example: `Finite (⋃ (i < n), f i)` where `f : ℕ → Set α` and `[∀ i, Finite (f i)]`
(when given instances from `Order.Interval.Finset.Nat`).
-/
instance finite_biUnion'' {ι : Type*} (p : ι → Prop) [h : Finite { x | p x }] (t : ι → Set α)
    [∀ i, Finite (t i)] : Finite (⋃ (x) (_ : p x), t x) :=
  @Finite.Set.finite_biUnion' _ _ (setOf p) h t _

Finite Union of Finite Sets over a Finite Predicate

Informal description

For any type $\iota$, a predicate $p$ on $\iota$ such that the set $\{x \mid p(x)\}$ is finite, and a family of sets $t : \iota \to \text{Set } \alpha$ where each $t(i)$ is finite, the union $\bigcup_{x \text{ with } p(x)} t(x)$ is finite.

Finite.Set.finite_iInter instance

{ι : Sort*} [Nonempty ι] (t : ι → Set α) [∀ i, Finite (t i)] : Finite (⋂ i, t i)

Full source

instance finite_iInter {ι : Sort*} [Nonempty ι] (t : ι → Set α) [∀ i, Finite (t i)] :
    Finite (⋂ i, t i) :=
  Finite.Set.subset (t <| Classical.arbitrary ι) (iInter_subset _ _)

Finite Intersection of Finite Sets is Finite

Informal description

For any nonempty index type $\iota$ and a family of sets $(t_i)_{i \in \iota}$ in a type $\alpha$, if each set $t_i$ is finite, then the intersection $\bigcap_{i} t_i$ is also finite.

Set.finite_iUnion theorem

[Finite ι] {f : ι → Set α} (H : ∀ i, (f i).Finite) : (⋃ i, f i).Finite

Full source

theorem finite_iUnion [Finite ι] {f : ι → Set α} (H : ∀ i, (f i).Finite) : (⋃ i, f i).Finite :=
  haveI := fun i => (H i).to_subtype
  toFinite _

Finite Union of Finite Sets is Finite

Informal description

For any finite index type $\iota$ and a family of sets $\{f(i)\}_{i \in \iota}$ in a type $\alpha$, if each set $f(i)$ is finite, then their union $\bigcup_{i \in \iota} f(i)$ is finite.

Set.Finite.biUnion' theorem

 {ι} {s : Set ι} (hs : s.Finite) {t : ∀ i ∈ s, Set α} (ht : ∀ i (hi : i ∈ s), (t i hi).Finite) :
  (⋃ i ∈ s, t i ‹_›).Finite

Full source

/-- Dependent version of `Finite.biUnion`. -/
theorem Finite.biUnion' {ι} {s : Set ι} (hs : s.Finite) {t : ∀ i ∈ s, Set α}
    (ht : ∀ i (hi : i ∈ s), (t i hi).Finite) : (⋃ i ∈ s, t i ‹_›).Finite := by
  have := hs.to_subtype
  rw [biUnion_eq_iUnion]
  apply finite_iUnion fun i : s => ht i.1 i.2

Finite Union of Finite Indexed Sets is Finite

Informal description

Let $\iota$ be a type and $s \subseteq \iota$ be a finite set. Given a family of sets $\{t_i\}_{i \in s}$ in a type $\alpha$ such that each $t_i$ is finite, the union $\bigcup_{i \in s} t_i$ is finite.

Set.Finite.biUnion theorem

{ι} {s : Set ι} (hs : s.Finite) {t : ι → Set α} (ht : ∀ i ∈ s, (t i).Finite) : (⋃ i ∈ s, t i).Finite

Full source

theorem Finite.biUnion {ι} {s : Set ι} (hs : s.Finite) {t : ι → Set α}
    (ht : ∀ i ∈ s, (t i).Finite) : (⋃ i ∈ s, t i).Finite :=
  hs.biUnion' ht

Finite Union of Finite Indexed Sets

Informal description

Let $\iota$ be a type and $s \subseteq \iota$ be a finite set. Given a family of sets $\{t_i\}_{i \in \iota}$ in a type $\alpha$ such that for each $i \in s$, the set $t_i$ is finite, then the union $\bigcup_{i \in s} t_i$ is finite.

Set.Finite.sUnion theorem

{s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, Set.Finite t) : (⋃₀ s).Finite

Full source

theorem Finite.sUnion {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, Set.Finite t) :
    (⋃₀ s).Finite := by
  simpa only [sUnion_eq_biUnion] using hs.biUnion H

Finite Union of Finite Sets is Finite

Informal description

Let $s$ be a finite collection of sets in a type $\alpha$, and suppose that every set $t \in s$ is finite. Then the union $\bigcup_{t \in s} t$ is finite.

Set.Finite.sInter theorem

{α : Type*} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) : (⋂₀ s).Finite

Full source

theorem Finite.sInter {α : Type*} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) :
    (⋂₀ s).Finite :=
  hf.subset (sInter_subset_of_mem ht)

Finiteness of Intersection of a Family of Sets with a Finite Member

Informal description

Let $s$ be a set of sets in a type $\alpha$, and let $t$ be a finite set belonging to $s$. Then the intersection of all sets in $s$, denoted $\bigcap₀ s$, is finite.

Set.Finite.iUnion theorem

 {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Finite) (hs : ∀ i ∈ t, (s i).Finite) (he : ∀ i, i ∉ t → s i = ∅) :
  (⋃ i, s i).Finite

Full source

/-- If sets `s i` are finite for all `i` from a finite set `t` and are empty for `i ∉ t`, then the
union `⋃ i, s i` is a finite set. -/
theorem Finite.iUnion {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Finite)
    (hs : ∀ i ∈ t, (s i).Finite) (he : ∀ i, i ∉ t → s i = ∅) : (⋃ i, s i).Finite := by
  suffices ⋃ i, s i⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this
  refine iUnion_subset fun i x hx => ?_
  by_cases hi : i ∈ t
  · exact mem_biUnion hi hx
  · rw [he i hi, mem_empty_iff_false] at hx
    contradiction

Finiteness of Union of Finite Indexed Sets with Finite Support

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of sets in a type $\alpha$, and let $t \subseteq \iota$ be a finite set. If for each $i \in t$, the set $s_i$ is finite, and for each $i \notin t$, the set $s_i$ is empty, then the union $\bigcup_{i \in \iota} s_i$ is finite.

Set.finite_iUnion_iff theorem

 {ι : Type*} {s : ι → Set α} (hs : Pairwise fun i j ↦ Disjoint (s i) (s j)) :
  (⋃ i, s i).Finite ↔ (∀ i, (s i).Finite) ∧ {i | (s i).Nonempty}.Finite

Full source

/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty. -/
lemma finite_iUnion_iff {ι : Type*} {s : ι → Set α} (hs : Pairwise fun i j ↦ Disjoint (s i) (s j)) :
    (⋃ i, s i).Finite ↔ (∀ i, (s i).Finite) ∧ {i | (s i).Nonempty}.Finite where
  mp h := by
    refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩
    let u (i : {i | (s i).Nonempty}) : ⋃ i, s i := ⟨i.2.choose, mem_iUnion.2 ⟨i.1, i.2.choose_spec⟩⟩
    have u_inj : Function.Injective u := by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      ext
      refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
      rw [hij]
      exact hj.choose_spec
    have : Finite (⋃ i, s i) := h
    exact .of_injective u u_inj
  mpr h := h.2.iUnion (fun _ _ ↦ h.1 _) (by simp [not_nonempty_iff_eq_empty])

Finiteness Criterion for Pairwise Disjoint Unions

Informal description

Let $\{s_i\}_{i \in \iota}$ be a pairwise disjoint family of sets in a type $\alpha$. Then the union $\bigcup_{i \in \iota} s_i$ is finite if and only if: 1. Each set $s_i$ is finite for all $i \in \iota$, and 2. The set $\{i \in \iota \mid s_i \neq \emptyset\}$ is finite.

Set.finite_iUnion_of_subsingleton theorem

{ι : Sort*} [Subsingleton ι] {s : ι → Set α} : (⋃ i, s i).Finite ↔ ∀ i, (s i).Finite

Full source

@[simp] lemma finite_iUnion_of_subsingleton {ι : Sort*} [Subsingleton ι] {s : ι → Set α} :
    (⋃ i, s i).Finite ↔ ∀ i, (s i).Finite := by
  rw [← iUnion_plift_down, finite_iUnion_iff _root_.Subsingleton.pairwise]
  simp [PLift.forall, Finite.of_subsingleton]

Finiteness of Union over Subsingleton Index Type

Informal description

For a subsingleton type $\iota$ (i.e., a type with at most one element) and a family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, the union $\bigcup_{i \in \iota} s_i$ is finite if and only if each set $s_i$ is finite for all $i \in \iota$.

Set.PairwiseDisjoint.finite_biUnion_iff theorem

 {f : β → Set α} {s : Set β} (hs : s.PairwiseDisjoint f) :
  (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i ∈ s | (f i).Nonempty}.Finite

Full source

/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty. -/
lemma PairwiseDisjoint.finite_biUnion_iff {f : β → Set α} {s : Set β} (hs : s.PairwiseDisjoint f) :
    (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i ∈ s | (f i).Nonempty}.Finite := by
  rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]
  simp

Finiteness Criterion for Pairwise Disjoint Unions of Indexed Sets

Informal description

Let $f \colon \beta \to \text{Set} \alpha$ be a function and $s \subseteq \beta$ a set such that $s$ is pairwise disjoint under $f$. Then the union $\bigcup_{i \in s} f(i)$ is finite if and only if: 1. For every $i \in s$, the set $f(i)$ is finite, and 2. The set $\{i \in s \mid f(i) \neq \emptyset\}$ is finite.

Set.Finite.preimage' theorem

(h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' { b }).Finite) : (f ⁻¹' s).Finite

Full source

theorem Finite.preimage' (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) :
    (f ⁻¹' s).Finite := by
  rw [← Set.biUnion_preimage_singleton]
  exact Set.Finite.biUnion h hf

Finiteness of Preimage under Finite Fibers Condition

Informal description

Let $f \colon \alpha \to \beta$ be a function and $s \subseteq \beta$ a finite set. If for every $b \in s$, the preimage $f^{-1}(\{b\})$ is finite, then the preimage $f^{-1}(s)$ is finite.

Set.union_finset_finite_of_range_finite theorem

(f : α → Finset β) (h : (range f).Finite) : (⋃ a, (f a : Set β)).Finite

Full source

/-- A finite union of finsets is finite. -/
theorem union_finset_finite_of_range_finite (f : α → Finset β) (h : (range f).Finite) :
    (⋃ a, (f a : Set β)).Finite := by
  rw [← biUnion_range]
  exact h.biUnion fun y _ => y.finite_toSet

Finite Union of Finsets with Finite Range

Informal description

For any function $f \colon \alpha \to \text{Finset} \beta$ with finite range, the union $\bigcup_{a \in \alpha} (f(a) : \text{Set} \beta)$ is finite.

Set.Finite.of_finite_fibers theorem

 (f : α → β) {s : Set α} (himage : (f '' s).Finite) (hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' { x }).Finite) : s.Finite

Full source

/--
If the image of `s` under `f` is finite, and each fiber of `f` has a finite intersection
with `s`, then `s` is itself finite.

It is useful to give `f` explicitly here so this can be used with `apply`.
-/
lemma Finite.of_finite_fibers (f : α → β) {s : Set α} (himage : (f '' s).Finite)
    (hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite) : s.Finite :=
  (himage.biUnion hfibers).subset fun x ↦ by aesop

Finiteness via Finite Fibers and Finite Image

Informal description

Let $f : \alpha \to \beta$ be a function and $s \subseteq \alpha$ be a subset. If the image $f(s)$ is finite and for every $x \in f(s)$, the fiber $s \cap f^{-1}(\{x\})$ is finite, then $s$ is finite.

Set.finite_subset_iUnion theorem

 {s : Set α} (hs : s.Finite) {ι} {t : ι → Set α} (h : s ⊆ ⋃ i, t i) : ∃ I : Set ι, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Full source

theorem finite_subset_iUnion {s : Set α} (hs : s.Finite) {ι} {t : ι → Set α} (h : s ⊆ ⋃ i, t i) :
    ∃ I : Set ι, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i := by
  have := hs.to_subtype
  choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
  refine ⟨range f, finite_range f, fun x hx => ?_⟩
  rw [biUnion_range, mem_iUnion]
  exact ⟨⟨x, hx⟩, hf _⟩

Finite Subset of Union Admits Finite Subcover

Informal description

For any finite set $s \subseteq \alpha$ and any family of sets $\{t_i\}_{i \in \iota}$ indexed by $\iota$, if $s$ is contained in the union $\bigcup_{i \in \iota} t_i$, then there exists a finite subset $I \subseteq \iota$ such that $s \subseteq \bigcup_{i \in I} t_i$.

Set.infinite_iUnion theorem

{ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) : (⋃ i, s i).Infinite

Full source

theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) :
    (⋃ i, s i).Infinite :=
  fun hfin ↦ @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype
    (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun i j h_eq ↦ hs (by simpa using h_eq)

Infinite Union of Injective Family is Infinite

Informal description

Let $\iota$ be an infinite type and $\{s_i\}_{i \in \iota}$ be a family of sets in $\alpha$. If the indexing function $s : \iota \to \text{Set } \alpha$ is injective, then the union $\bigcup_{i \in \iota} s_i$ is infinite.

Set.Infinite.biUnion theorem

{ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite) (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite

Full source

theorem Infinite.biUnion {ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite)
    (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite := by
  rw [biUnion_eq_iUnion]
  have _ := ha.to_subtype
  exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]

Infinite Bounded Union of Injective Family is Infinite

Informal description

Let $\iota$ be a type and $\{s_i\}_{i \in \iota}$ be a family of sets in $\alpha$. If the set $a \subseteq \iota$ is infinite and the function $s$ is injective on $a$, then the union $\bigcup_{i \in a} s_i$ is infinite.

Set.Infinite.sUnion theorem

{s : Set (Set α)} (hs : s.Infinite) : (⋃₀ s).Infinite

Full source

theorem Infinite.sUnion {s : Set (Set α)} (hs : s.Infinite) : (⋃₀ s).Infinite := by
  rw [sUnion_eq_iUnion]
  have _ := hs.to_subtype
  exact infinite_iUnion Subtype.coe_injective

Infinite Union of Infinite Family is Infinite

Informal description

Let $\mathcal{S}$ be an infinite family of sets in $\alpha$. Then the union $\bigcup \mathcal{S}$ is infinite.

Set.map_finite_biSup theorem

 {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [SupBotHomClass F α β] {s : Set ι}
  (hs : s.Finite) (f : F) (g : ι → α) : f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)

Full source

lemma map_finite_biSup {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [SupBotHomClass F α β] {s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) :
    f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x) := by
  have := map_finset_sup f hs.toFinset g
  simp only [Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply] at this
  exact this

Supremum-Preserving Morphism Commutes with Finite Suprema

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $F$ be a type of morphisms from $\alpha$ to $\beta$ that preserves finite suprema and the bottom element. For any finite set $s$ of indices and any function $g : \iota \to \alpha$, the morphism $f \in F$ satisfies \[ f\left(\bigvee_{x \in s} g(x)\right) = \bigvee_{x \in s} f(g(x)). \]

Set.map_finite_biInf theorem

 {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [InfTopHomClass F α β] {s : Set ι}
  (hs : s.Finite) (f : F) (g : ι → α) : f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Full source

lemma map_finite_biInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [InfTopHomClass F α β] {s : Set ι} (hs : s.Finite) (f : F) (g : ι → α) :
    f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x) := by
  have := map_finset_inf f hs.toFinset g
  simp only [Finset.inf_eq_iInf, hs.mem_toFinset, comp_apply] at this
  exact this

Infimum-Preserving Morphism Commutes with Finite Infima

Informal description

Let $F$ be a type of morphisms between complete lattices $\alpha$ and $\beta$ that preserves finite infima and the top element. For any finite set $s$ of indices and any function $g : \iota \to \alpha$, the infimum-preserving morphism $f \in F$ satisfies \[ f\left(\bigwedge_{x \in s} g(x)\right) = \bigwedge_{x \in s} f(g(x)). \]

Set.map_finite_iSup theorem

 {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [SupBotHomClass F α β] [Finite ι] (f : F)
  (g : ι → α) : f (⨆ i, g i) = ⨆ i, f (g i)

Full source

lemma map_finite_iSup {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [SupBotHomClass F α β] [Finite ι] (f : F) (g : ι → α) :
    f (⨆ i, g i) = ⨆ i, f (g i) := by
  rw [← iSup_univ (f := g), ← iSup_univ (f := fun i ↦ f (g i))]
  exact map_finite_biSup finite_univ f g

Supremum-Preserving Morphism Commutes with Finite Suprema over Finite Types

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $F$ be a type of morphisms from $\alpha$ to $\beta$ that preserves finite suprema and the bottom element. For any finite type $\iota$ and any function $g : \iota \to \alpha$, the morphism $f \in F$ satisfies \[ f\left(\bigvee_{i \in \iota} g(i)\right) = \bigvee_{i \in \iota} f(g(i)). \]

Set.map_finite_iInf theorem

 {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β] [InfTopHomClass F α β] [Finite ι] (f : F)
  (g : ι → α) : f (⨅ i, g i) = ⨅ i, f (g i)

Full source

lemma map_finite_iInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [InfTopHomClass F α β] [Finite ι] (f : F) (g : ι → α) :
    f (⨅ i, g i) = ⨅ i, f (g i) := by
  rw [← iInf_univ (f := g), ← iInf_univ (f := fun i ↦ f (g i))]
  exact map_finite_biInf finite_univ f g

Infimum-Preserving Morphism Commutes with Finite Infima over Finite Types

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $F$ be a type of morphisms from $\alpha$ to $\beta$ that preserves finite infima and the top element. For any finite type $\iota$ and any function $g : \iota \to \alpha$, the morphism $f \in F$ satisfies \[ f\left(\bigwedge_{i \in \iota} g(i)\right) = \bigwedge_{i \in \iota} f(g(i)). \]

Set.Finite.iSup_biInf_of_monotone theorem

 {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Frame α] {s : Set ι} (hs : s.Finite)
  {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j

Full source

theorem Finite.iSup_biInf_of_monotone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (· ≤ ·)] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α}
    (hf : ∀ i ∈ s, Monotone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j := by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp [iSup_const]
  | insert _ _ ihs =>
    rw [forall_mem_insert] at hf
    simp only [iInf_insert, ← ihs hf.2]
    exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

Finite Monotone Interchange of Supremum and Infimum in Frames

Informal description

Let $\iota$ and $\iota'$ be types, where $\iota'$ is equipped with a preorder and is nonempty and directed with respect to this order. Let $\alpha$ be a complete lattice satisfying the frame condition. Given a finite set $s \subseteq \iota$ and a family of monotone functions $f_i : \iota' \to \alpha$ indexed by $i \in s$, the following equality holds: \[ \bigvee_{j \in \iota'} \bigwedge_{i \in s} f_i(j) = \bigwedge_{i \in s} \bigvee_{j \in \iota'} f_i(j). \]

Set.Finite.iSup_biInf_of_antitone theorem

 {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))] [Order.Frame α] {s : Set ι} (hs : s.Finite)
  {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j

Full source

theorem Finite.iSup_biInf_of_antitone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (swap (· ≤ ·))] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α}
    (hf : ∀ i ∈ s, Antitone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j :=
  @Finite.iSup_biInf_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ hs _ fun i hi => (hf i hi).dual_left

Finite Antitone Interchange of Supremum and Infimum in Frames

Informal description

Let $\iota$ and $\iota'$ be types, where $\iota'$ is equipped with a preorder and is nonempty and directed with respect to the dual order (i.e., $\geq$). Let $\alpha$ be a complete lattice satisfying the frame condition. Given a finite set $s \subseteq \iota$ and a family of antitone functions $f_i : \iota' \to \alpha$ indexed by $i \in s$, the following equality holds: \[ \bigvee_{j \in \iota'} \bigwedge_{i \in s} f_i(j) = \bigwedge_{i \in s} \bigvee_{j \in \iota'} f_i(j). \]

Set.Finite.iInf_biSup_of_monotone theorem

 {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))] [Order.Coframe α] {s : Set ι}
  (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) : ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j

Full source

theorem Finite.iInf_biSup_of_monotone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (swap (· ≤ ·))] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α}
    (hf : ∀ i ∈ s, Monotone (f i)) : ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j :=
  hs.iSup_biInf_of_antitone (α := αᵒᵈ) fun i hi => (hf i hi).dual_right

Finite Monotone Interchange of Infimum and Supremum in Coframes

Informal description

Let $\iota$ and $\iota'$ be types, where $\iota'$ is equipped with a preorder and is nonempty and directed with respect to the dual order (i.e., $\geq$). Let $\alpha$ be a complete lattice satisfying the coframe condition. Given a finite set $s \subseteq \iota$ and a family of monotone functions $f_i : \iota' \to \alpha$ indexed by $i \in s$, the following equality holds: \[ \bigwedge_{j \in \iota'} \bigvee_{i \in s} f_i(j) = \bigvee_{i \in s} \bigwedge_{j \in \iota'} f_i(j). \]

Set.Finite.iInf_biSup_of_antitone theorem

 {ι ι' α : Type*} [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Coframe α] {s : Set ι} (hs : s.Finite)
  {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) : ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j

Full source

theorem Finite.iInf_biSup_of_antitone {ι ι' α : Type*} [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (· ≤ ·)] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α}
    (hf : ∀ i ∈ s, Antitone (f i)) : ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j :=
  hs.iSup_biInf_of_monotone (α := αᵒᵈ) fun i hi => (hf i hi).dual_right

Finite Antitone Interchange of Infimum and Supremum in Coframes

Informal description

Let $\iota$ and $\iota'$ be types, where $\iota'$ is equipped with a preorder and is nonempty and directed with respect to this order. Let $\alpha$ be a complete lattice satisfying the coframe condition. Given a finite set $s \subseteq \iota$ and a family of antitone functions $f_i : \iota' \to \alpha$ indexed by $i \in s$, the following equality holds: \[ \bigwedge_{j \in \iota'} \bigvee_{i \in s} f_i(j) = \bigvee_{i \in s} \bigwedge_{j \in \iota'} f_i(j). \]

Set.iSup_iInf_of_monotone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Frame α] {f : ι → ι' → α}
  (hf : ∀ i, Monotone (f i)) : ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j

Full source

theorem iSup_iInf_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (· ≤ ·)] [Order.Frame α] {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) :
    ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j := by
  simpa only [iInf_univ] using finite_univ.iSup_biInf_of_monotone fun i _ => hf i

Finite Monotone Interchange of Supremum and Infimum in Frames

Informal description

Let $\iota$ be a finite type, $\iota'$ a preordered nonempty directed type, and $\alpha$ a complete lattice satisfying the frame condition. Given a family of monotone functions $f_i : \iota' \to \alpha$ indexed by $i \in \iota$, the following equality holds: \[ \bigvee_{j \in \iota'} \bigwedge_{i \in \iota} f_i(j) = \bigwedge_{i \in \iota} \bigvee_{j \in \iota'} f_i(j). \]

Set.iSup_iInf_of_antitone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))] [Order.Frame α] {f : ι → ι' → α}
  (hf : ∀ i, Antitone (f i)) : ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j

Full source

theorem iSup_iInf_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (swap (· ≤ ·))] [Order.Frame α] {f : ι → ι' → α} (hf : ∀ i, Antitone (f i)) :
    ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j :=
  @iSup_iInf_of_monotone ι ι'ᵒᵈ α _ _ _ _ _ _ fun i => (hf i).dual_left

Finite Antitone Interchange of Supremum and Infimum in Frames

Informal description

Let $\iota$ be a finite type, $\iota'$ a nonempty preordered type directed with respect to the reverse order, and $\alpha$ a complete lattice satisfying the frame condition. Given a family of antitone functions $f_i : \iota' \to \alpha$ indexed by $i \in \iota$, the following equality holds: \[ \bigvee_{j \in \iota'} \bigwedge_{i \in \iota} f_i(j) = \bigwedge_{i \in \iota} \bigvee_{j \in \iota'} f_i(j). \]

Set.iInf_iSup_of_monotone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (swap (· ≤ ·))] [Order.Coframe α]
  {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) : ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j

Full source

theorem iInf_iSup_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (swap (· ≤ ·))] [Order.Coframe α] {f : ι → ι' → α} (hf : ∀ i, Monotone (f i)) :
    ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j :=
  iSup_iInf_of_antitone (α := αᵒᵈ) fun i => (hf i).dual_right

Monotone Interchange of Infimum and Supremum in Coframes for Finite Index Sets

Informal description

Let $\iota$ be a finite type, $\iota'$ a nonempty preordered type directed with respect to the reverse order, and $\alpha$ a coframe. Given a family of monotone functions $f_i : \iota' \to \alpha$ indexed by $i \in \iota$, the following equality holds: \[ \bigwedge_{j \in \iota'} \bigvee_{i \in \iota} f_i(j) = \bigvee_{i \in \iota} \bigwedge_{j \in \iota'} f_i(j). \]

Set.iInf_iSup_of_antitone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι'] [IsDirected ι' (· ≤ ·)] [Order.Coframe α] {f : ι → ι' → α}
  (hf : ∀ i, Antitone (f i)) : ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j

Full source

theorem iInf_iSup_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [Nonempty ι']
    [IsDirected ι' (· ≤ ·)] [Order.Coframe α] {f : ι → ι' → α} (hf : ∀ i, Antitone (f i)) :
    ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j :=
  iSup_iInf_of_monotone (α := αᵒᵈ) fun i => (hf i).dual_right

Antitone Interchange of Infimum and Supremum in Coframes for Finite Index Sets

Informal description

Let $\iota$ be a finite type, $\iota'$ a nonempty directed preorder, and $\alpha$ a coframe. Given a family of antitone functions $f_i : \iota' \to \alpha$ indexed by $i \in \iota$, the following equality holds: \[ \bigwedge_{j \in \iota'} \bigvee_{i \in \iota} f_i(j) = \bigvee_{i \in \iota} \bigwedge_{j \in \iota'} f_i(j). \]

Set.iUnion_iInter_of_monotone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (· ≤ ·)] [Nonempty ι'] {s : ι → ι' → Set α}
  (hs : ∀ i, Monotone (s i)) : ⋃ j : ι', ⋂ i : ι, s i j = ⋂ i : ι, ⋃ j : ι', s i j

Full source

/-- An increasing union distributes over finite intersection. -/
theorem iUnion_iInter_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (· ≤ ·)]
    [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ i, Monotone (s i)) :
    ⋃ j : ι', ⋂ i : ι, s i j = ⋂ i : ι, ⋃ j : ι', s i j :=
  iSup_iInf_of_monotone hs

Monotone Union-Intersection Exchange for Finite Families of Sets

Informal description

Let $\iota$ be a finite type and $\iota'$ a nonempty directed preorder. Given a family of sets $s_i : \iota' \to \text{Set}(\alpha)$ indexed by $i \in \iota$ such that each $s_i$ is monotone (i.e., $j \leq j'$ implies $s_i(j) \subseteq s_i(j')$), the following equality holds: \[ \bigcup_{j \in \iota'} \bigcap_{i \in \iota} s_i(j) = \bigcap_{i \in \iota} \bigcup_{j \in \iota'} s_i(j). \]

Set.iUnion_iInter_of_antitone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (swap (· ≤ ·))] [Nonempty ι'] {s : ι → ι' → Set α}
  (hs : ∀ i, Antitone (s i)) : ⋃ j : ι', ⋂ i : ι, s i j = ⋂ i : ι, ⋃ j : ι', s i j

Full source

/-- A decreasing union distributes over finite intersection. -/
theorem iUnion_iInter_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι']
    [IsDirected ι' (swap (· ≤ ·))] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ i, Antitone (s i)) :
    ⋃ j : ι', ⋂ i : ι, s i j = ⋂ i : ι, ⋃ j : ι', s i j :=
  iSup_iInf_of_antitone hs

Antitone Union-Intersection Exchange for Finite Families of Sets

Informal description

Let $\iota$ be a finite type and $\iota'$ a nonempty preordered type directed with respect to the reverse order. Given a family of antitone set-valued functions $s_i : \iota' \to \text{Set}(\alpha)$ indexed by $i \in \iota$ (i.e., for each $i$, $j \leq j'$ implies $s_i(j') \subseteq s_i(j)$), the following equality holds: \[ \bigcup_{j \in \iota'} \bigcap_{i \in \iota} s_i(j) = \bigcap_{i \in \iota} \bigcup_{j \in \iota'} s_i(j). \]

Set.iInter_iUnion_of_monotone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (swap (· ≤ ·))] [Nonempty ι'] {s : ι → ι' → Set α}
  (hs : ∀ i, Monotone (s i)) : ⋂ j : ι', ⋃ i : ι, s i j = ⋃ i : ι, ⋂ j : ι', s i j

Full source

/-- An increasing intersection distributes over finite union. -/
theorem iInter_iUnion_of_monotone {ι ι' α : Type*} [Finite ι] [Preorder ι']
    [IsDirected ι' (swap (· ≤ ·))] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ i, Monotone (s i)) :
    ⋂ j : ι', ⋃ i : ι, s i j = ⋃ i : ι, ⋂ j : ι', s i j :=
  iInf_iSup_of_monotone hs

Monotone Intersection-Union Exchange for Finite Families of Sets

Informal description

Let $\iota$ be a finite type and $\iota'$ a nonempty preordered type directed with respect to the reverse order. Given a family of monotone set-valued functions $s_i : \iota' \to \text{Set}(\alpha)$ indexed by $i \in \iota$ (i.e., for each $i$, $j \leq j'$ implies $s_i(j) \subseteq s_i(j')$), the following equality holds: \[ \bigcap_{j \in \iota'} \bigcup_{i \in \iota} s_i(j) = \bigcup_{i \in \iota} \bigcap_{j \in \iota'} s_i(j). \]

Set.iInter_iUnion_of_antitone theorem

 {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (· ≤ ·)] [Nonempty ι'] {s : ι → ι' → Set α}
  (hs : ∀ i, Antitone (s i)) : ⋂ j : ι', ⋃ i : ι, s i j = ⋃ i : ι, ⋂ j : ι', s i j

Full source

/-- A decreasing intersection distributes over finite union. -/
theorem iInter_iUnion_of_antitone {ι ι' α : Type*} [Finite ι] [Preorder ι'] [IsDirected ι' (· ≤ ·)]
    [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ i, Antitone (s i)) :
    ⋂ j : ι', ⋃ i : ι, s i j = ⋃ i : ι, ⋂ j : ι', s i j :=
  iInf_iSup_of_antitone hs

Antitone Interchange of Intersection and Union for Finite Index Sets

Informal description

Let $\iota$ be a finite type, $\iota'$ a nonempty directed preorder, and $\alpha$ a type. Given a family of antitone functions $s_i : \iota' \to \text{Set } \alpha$ indexed by $i \in \iota$, the following equality holds: \[ \bigcap_{j \in \iota'} \bigcup_{i \in \iota} s_i(j) = \bigcup_{i \in \iota} \bigcap_{j \in \iota'} s_i(j). \]

Set.iUnion_pi_of_monotone theorem

 {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type*} {I : Set ι} {s : ∀ i, ι' → Set (α i)} (hI : I.Finite)
  (hs : ∀ i ∈ I, Monotone (s i)) : ⋃ j : ι', I.pi (fun i => s i j) = I.pi fun i => ⋃ j, s i j

Full source

theorem iUnion_pi_of_monotone {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type*}
    {I : Set ι} {s : ∀ i, ι' → Set (α i)} (hI : I.Finite) (hs : ∀ i ∈ I, Monotone (s i)) :
    ⋃ j : ι', I.pi (fun i => s i j) = I.pi fun i => ⋃ j, s i j := by
  simp only [pi_def, biInter_eq_iInter, preimage_iUnion]
  haveI := hI.fintype.finite
  refine iUnion_iInter_of_monotone (ι' := ι') (fun (i : I) j₁ j₂ h => ?_)
  exact preimage_mono <| hs i i.2 h

Monotone Union-Cartesian Product Interchange for Finite Index Sets

Informal description

Let $\iota$ and $\iota'$ be types, with $\iota'$ a nonempty linear order. Let $\{\alpha_i\}_{i \in \iota}$ be a family of types, and let $I \subseteq \iota$ be a finite subset. Given a family of sets $\{s_i(j)\}_{j \in \iota'}$ in $\alpha_i$ for each $i \in I$, where each $s_i$ is monotone (i.e., $j \leq j'$ implies $s_i(j) \subseteq s_i(j')$), the following equality holds: \[ \bigcup_{j \in \iota'} \left( \prod_{i \in I} s_i(j) \right) = \prod_{i \in I} \left( \bigcup_{j \in \iota'} s_i(j) \right). \] Here, $\prod_{i \in I} s_i(j)$ denotes the Cartesian product of the sets $s_i(j)$ for $i \in I$.

Set.iUnion_univ_pi_of_monotone theorem

 {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] [Finite ι] {α : ι → Type*} {s : ∀ i, ι' → Set (α i)}
  (hs : ∀ i, Monotone (s i)) : ⋃ j : ι', pi univ (fun i => s i j) = pi univ fun i => ⋃ j, s i j

Full source

theorem iUnion_univ_pi_of_monotone {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] [Finite ι]
    {α : ι → Type*} {s : ∀ i, ι' → Set (α i)} (hs : ∀ i, Monotone (s i)) :
    ⋃ j : ι', pi univ (fun i => s i j) = pi univ fun i => ⋃ j, s i j :=
  iUnion_pi_of_monotone finite_univ fun i _ => hs i

Monotone Union-Cartesian Product Interchange for Finite Types

Informal description

Let $\iota$ and $\iota'$ be types, with $\iota'$ a nonempty linear order and $\iota$ a finite type. Let $\{\alpha_i\}_{i \in \iota}$ be a family of types. Given a family of sets $\{s_i(j)\}_{j \in \iota'}$ in $\alpha_i$ for each $i \in \iota$, where each $s_i$ is monotone (i.e., $j \leq j'$ implies $s_i(j) \subseteq s_i(j')$), the following equality holds: \[ \bigcup_{j \in \iota'} \left( \prod_{i \in \iota} s_i(j) \right) = \prod_{i \in \iota} \left( \bigcup_{j \in \iota'} s_i(j) \right). \] Here, $\prod_{i \in \iota} s_i(j)$ denotes the Cartesian product of the sets $s_i(j)$ for $i \in \iota$.

Set.Finite.bddAbove theorem

(hs : s.Finite) : BddAbove s

Full source

/-- A finite set is bounded above. -/
protected theorem Finite.bddAbove (hs : s.Finite) : BddAbove s :=
  Finite.induction_on _ hs bddAbove_empty fun _ _ h => h.insert _

Finite sets are bounded above

Informal description

For any finite set $s$ in a type with a preorder, $s$ is bounded above.

Set.Finite.bddAbove_biUnion theorem

{I : Set β} {S : β → Set α} (H : I.Finite) : BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i)

Full source

/-- A finite union of sets which are all bounded above is still bounded above. -/
theorem Finite.bddAbove_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
    BddAboveBddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i) := by
  induction I, H using Set.Finite.induction_on with
  | empty => simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]
  | insert _ _ hs => simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

Finite Union is Bounded Above if and only if Each Set is Bounded Above

Informal description

Let $I$ be a finite set and $\{S_i\}_{i \in I}$ be a family of sets in a type $\alpha$ with an order structure. The union $\bigcup_{i \in I} S_i$ is bounded above if and only if each $S_i$ is bounded above for all $i \in I$.

Set.infinite_of_not_bddAbove theorem

: ¬BddAbove s → s.Infinite

Full source

theorem infinite_of_not_bddAbove : ¬BddAbove s → s.Infinite :=
  mt Finite.bddAbove

Unbounded Sets are Infinite

Informal description

If a set $s$ is not bounded above in a type with a preorder, then $s$ is infinite.

Set.Finite.bddBelow theorem

(hs : s.Finite) : BddBelow s

Full source

/-- A finite set is bounded below. -/
protected theorem Finite.bddBelow (hs : s.Finite) : BddBelow s :=
  Finite.bddAbove (α := αᵒᵈ) hs

Finite sets are bounded below

Informal description

For any finite set $s$ in a type with a preorder, $s$ is bounded below.

Set.Finite.bddBelow_biUnion theorem

{I : Set β} {S : β → Set α} (H : I.Finite) : BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i)

Full source

/-- A finite union of sets which are all bounded below is still bounded below. -/
theorem Finite.bddBelow_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
    BddBelowBddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i) :=
  Finite.bddAbove_biUnion (α := αᵒᵈ) H

Finite Union is Bounded Below if and only if Each Set is Bounded Below

Informal description

Let $I$ be a finite set and $\{S_i\}_{i \in I}$ be a family of sets in a type $\alpha$ with an order structure. The union $\bigcup_{i \in I} S_i$ is bounded below if and only if each $S_i$ is bounded below for all $i \in I$.

Set.infinite_of_not_bddBelow theorem

: ¬BddBelow s → s.Infinite

Full source

theorem infinite_of_not_bddBelow : ¬BddBelow s → s.Infinite := mt Finite.bddBelow

Unbounded Below Sets are Infinite

Informal description

If a set $s$ is not bounded below, then $s$ is infinite.

Finset.bddAbove theorem

[SemilatticeSup α] [Nonempty α] (s : Finset α) : BddAbove (↑s : Set α)

Full source

/-- A finset is bounded above. -/
protected theorem bddAbove [SemilatticeSup α] [Nonempty α] (s : Finset α) : BddAbove (↑s : Set α) :=
  s.finite_toSet.bddAbove

Finite Sets are Bounded Above in Semilattices

Informal description

For any finite subset $s$ of a type $\alpha$ equipped with a semilattice supremum structure and a nonempty instance, the set $s$ is bounded above in $\alpha$.

Finset.bddBelow theorem

[SemilatticeInf α] [Nonempty α] (s : Finset α) : BddBelow (↑s : Set α)

Full source

/-- A finset is bounded below. -/
protected theorem bddBelow [SemilatticeInf α] [Nonempty α] (s : Finset α) : BddBelow (↑s : Set α) :=
  s.finite_toSet.bddBelow

Finite Sets are Bounded Below in Semilattices

Informal description

For any finite subset $s$ of a type $\alpha$ equipped with a semilattice infimum structure and a nonempty instance, the set $s$ is bounded below in $\alpha$.

Set.finite_diff_iUnion_Ioo theorem

(s : Set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Ioo x y).Finite

Full source

lemma Set.finite_diff_iUnion_Ioo (s : Set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Ioo x y).Finite :=
  Set.finite_of_forall_not_lt_lt fun _x hx _y hy _z hz hxy hyz => hy.2 <| mem_iUnion₂_of_mem hx.1 <|
    mem_iUnion₂_of_mem hz.1 ⟨hxy, hyz⟩

Finiteness of Set Minus Union of Open Intervals

Informal description

For any set $s$ in a preorder $\alpha$, the set difference $s \setminus \bigcup_{x, y \in s} (x, y)$ is finite, where $(x, y)$ denotes the open interval $\{z \in \alpha \mid x < z < y\}$.

Set.finite_diff_iUnion_Ioo' theorem

(s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).Finite

Full source

lemma Set.finite_diff_iUnion_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).Finite := by
  simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_diff_iUnion_Ioo

Finiteness of Set Minus Union of Open Intervals (Product Version)

Informal description

For any set $s$ in a preorder $\alpha$, the set difference $s \setminus \bigcup_{(x,y) \in s \times s} (x, y)$ is finite, where $(x, y)$ denotes the open interval $\{z \in \alpha \mid x < z < y\}$.

Directed.exists_mem_subset_of_finset_subset_biUnion theorem

 {α ι : Type*} [Nonempty ι] {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
  ∃ i, (s : Set α) ⊆ f i

Full source

lemma Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [Nonempty ι]
    {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
    ∃ i, (s : Set α) ⊆ f i := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons b t hbt iht =>
    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
    rcases h i j with ⟨k, hik, hjk⟩
    exact ⟨k, hik hi, hj.trans hjk⟩

Finite Subset Property for Directed Unions

Informal description

Let $\alpha$ and $\iota$ be types with $\iota$ nonempty. Given a directed family of sets $\{f_i\}_{i \in \iota}$ in $\alpha$ (directed under inclusion) and a finite set $s \subseteq \alpha$ such that $s \subseteq \bigcup_{i \in \iota} f_i$, there exists an index $i \in \iota$ such that $s \subseteq f_i$.

DirectedOn.exists_mem_subset_of_finset_subset_biUnion theorem

 {α ι : Type*} {f : ι → Set α} {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun i j => f i ⊆ f j) c) {s : Finset α}
  (hs : (s : Set α) ⊆ ⋃ i ∈ c, f i) : ∃ i ∈ c, (s : Set α) ⊆ f i

Full source

theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} {f : ι → Set α}
    {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun i j => f i ⊆ f j) c) {s : Finset α}
    (hs : (s : Set α) ⊆ ⋃ i ∈ c, f i) : ∃ i ∈ c, (s : Set α) ⊆ f i := by
  rw [Set.biUnion_eq_iUnion] at hs
  haveI := hn.coe_sort
  simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

Finite Subset Property for Directed Unions on Subsets

Informal description

Let $\alpha$ and $\iota$ be types, and let $c$ be a nonempty subset of $\iota$. Given a family of sets $\{f_i\}_{i \in \iota}$ in $\alpha$ that is directed on $c$ under inclusion (i.e., for any $i, j \in c$, there exists $k \in c$ such that $f_i \subseteq f_k$ and $f_j \subseteq f_k$), and a finite set $s \subseteq \alpha$ such that $s \subseteq \bigcup_{i \in c} f_i$, there exists an index $i \in c$ such that $s \subseteq f_i$.

Mathlib.Data.Set.Finite.Lattice

Implementation notes

Tags