Mathlib.Data.Set.Lattice

Set.mem_iUnion₂ theorem

{x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋃ (i) (j), s i j) ↔ ∃ i j, x ∈ s i j

Full source

theorem mem_iUnion₂ {x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋃ (i) (j), s i j) ↔ ∃ i j, x ∈ s i j := by
  simp_rw [mem_iUnion]

Characterization of Membership in Double-Indexed Union

Informal description

For an element $x$ of type $\gamma$ and a family of sets $s_i(j) \subseteq \gamma$ indexed by $i$ and $j$, we have that $x$ belongs to the union $\bigcup_{i,j} s_i(j)$ if and only if there exist indices $i$ and $j$ such that $x \in s_i(j)$.

Set.mem_iInter₂ theorem

{x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋂ (i) (j), s i j) ↔ ∀ i j, x ∈ s i j

Full source

theorem mem_iInter₂ {x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋂ (i) (j), s i j) ↔ ∀ i j, x ∈ s i j := by
  simp_rw [mem_iInter]

Characterization of Membership in Double-Indexed Intersection

Informal description

For any element $x$ of type $\gamma$ and any family of sets $s_i(j)$ indexed by $i$ and $j$, the element $x$ belongs to the intersection $\bigcap_{i,j} s_i(j)$ if and only if for every index $i$ and $j$, $x$ belongs to $s_i(j)$. In symbols: $$x \in \bigcap_{i,j} s_i(j) \leftrightarrow \forall i\, j, x \in s_i(j)$$

Set.mem_iUnion_of_mem theorem

{s : ι → Set α} {a : α} (i : ι) (ha : a ∈ s i) : a ∈ ⋃ i, s i

Full source

theorem mem_iUnion_of_mem {s : ι → Set α} {a : α} (i : ι) (ha : a ∈ s i) : a ∈ ⋃ i, s i :=
  mem_iUnion.2 ⟨i, ha⟩

Element in Union if in Some Set of the Family

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, if an element $a \in \alpha$ belongs to $s_i$ for some index $i \in \iota$, then $a$ belongs to the union $\bigcup_{i \in \iota} s_i$.

Set.mem_iUnion₂_of_mem theorem

{s : ∀ i, κ i → Set α} {a : α} {i : ι} (j : κ i) (ha : a ∈ s i j) : a ∈ ⋃ (i) (j), s i j

Full source

theorem mem_iUnion₂_of_mem {s : ∀ i, κ i → Set α} {a : α} {i : ι} (j : κ i) (ha : a ∈ s i j) :
    a ∈ ⋃ (i) (j), s i j :=
  mem_iUnion₂.2 ⟨i, j, ha⟩

Element in Double-Indexed Union if in Some Set of the Family

Informal description

For any family of sets $\{s_i(j)\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if an element $a \in \alpha$ belongs to $s_i(j)$ for some indices $i \in \iota$ and $j \in \kappa_i$, then $a$ belongs to the double-indexed union $\bigcup_{i,j} s_i(j)$.

Set.mem_iInter_of_mem theorem

{s : ι → Set α} {a : α} (h : ∀ i, a ∈ s i) : a ∈ ⋂ i, s i

Full source

theorem mem_iInter_of_mem {s : ι → Set α} {a : α} (h : ∀ i, a ∈ s i) : a ∈ ⋂ i, s i :=
  mem_iInter.2 h

Element in All Sets Implies Element in Their Intersection

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ and any element $a \in \alpha$, if $a$ belongs to $s_i$ for every $i \in \iota$, then $a$ belongs to the intersection $\bigcap_{i \in \iota} s_i$.

Set.mem_iInter₂_of_mem theorem

{s : ∀ i, κ i → Set α} {a : α} (h : ∀ i j, a ∈ s i j) : a ∈ ⋂ (i) (j), s i j

Full source

theorem mem_iInter₂_of_mem {s : ∀ i, κ i → Set α} {a : α} (h : ∀ i j, a ∈ s i j) :
    a ∈ ⋂ (i) (j), s i j :=
  mem_iInter₂.2 h

Element in All Double-Indexed Sets Implies Element in Their Intersection

Informal description

For any element $a$ of type $\alpha$ and any family of sets $\{s_i(j)\}_{i,j}$ indexed by $i$ and $j$, if $a$ belongs to $s_i(j)$ for every $i$ and $j$, then $a$ belongs to the double-indexed intersection $\bigcap_{i,j} s_i(j)$.

Set.iUnion_congr_Prop theorem

 {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iUnion f₁ = iUnion f₂

Full source

@[congr]
theorem iUnion_congr_Prop {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q)
    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iUnion f₁ = iUnion f₂ :=
  iSup_congr_Prop pq f

Equality of Unions under Propositional Equivalence

Informal description

For any two propositions $p$ and $q$ that are equivalent ($p \leftrightarrow q$), and for any families of sets $f₁ : p → \text{Set } α$ and $f₂ : q → \text{Set } α$ such that for all $x$, $f₁(\text{pq.mpr } x) = f₂(x)$, the union of $f₁$ equals the union of $f₂$, i.e., $$\bigcup_{x \in p} f₁(x) = \bigcup_{x \in q} f₂(x).$$

Set.iInter_congr_Prop theorem

 {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iInter f₁ = iInter f₂

Full source

@[congr]
theorem iInter_congr_Prop {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q)
    (f : ∀ x, f₁ (pq.mpr x) = f₂ x) : iInter f₁ = iInter f₂ :=
  iInf_congr_Prop pq f

Equality of Intersections under Propositional Equivalence

Informal description

For any two propositions $p$ and $q$ that are equivalent (i.e., $p \leftrightarrow q$), and for any two families of sets $f₁ : p \to \text{Set } \alpha$ and $f₂ : q \to \text{Set } \alpha$ such that $f₁(pq.mpr(x)) = f₂(x)$ for all $x$, the intersection of the sets in $f₁$ is equal to the intersection of the sets in $f₂$. That is, \[ \bigcap_{x:p} f₁(x) = \bigcap_{x:q} f₂(x). \]

Set.iUnion_plift_up theorem

(f : PLift ι → Set α) : ⋃ i, f (PLift.up i) = ⋃ i, f i

Full source

theorem iUnion_plift_up (f : PLift ι → Set α) : ⋃ i, f (PLift.up i) = ⋃ i, f i :=
  iSup_plift_up _

Union Equality for Lifted Index Sets

Informal description

For any family of sets $f$ indexed by lifted elements of type $\iota$, the union of $f$ over all lifted elements is equal to the union of $f$ over all elements of $\iota$. That is, $\bigcup_{i} f(\text{PLift.up}(i)) = \bigcup_{i} f(i)$.

Set.iUnion_plift_down theorem

(f : ι → Set α) : ⋃ i, f (PLift.down i) = ⋃ i, f i

Full source

theorem iUnion_plift_down (f : ι → Set α) : ⋃ i, f (PLift.down i) = ⋃ i, f i :=
  iSup_plift_down _

Union Invariance under PLift Projection

Informal description

For any family of sets $\{f(i)\}_{i \in \iota}$ indexed by a type $\iota$, the union $\bigcup_{i \in \iota} f(\text{PLift.down}(i))$ is equal to $\bigcup_{i \in \iota} f(i)$, where $\text{PLift.down}$ is the canonical projection from the lifted type.

Set.iInter_plift_up theorem

(f : PLift ι → Set α) : ⋂ i, f (PLift.up i) = ⋂ i, f i

Full source

theorem iInter_plift_up (f : PLift ι → Set α) : ⋂ i, f (PLift.up i) = ⋂ i, f i :=
  iInf_plift_up _

Intersection Equality Under Index Lifting

Informal description

For any family of sets $f$ indexed by lifted elements of type $\iota$, the intersection over all lifted indices equals the intersection over all original indices. That is, \[ \bigcap_{i} f(\mathrm{PLift.up}(i)) = \bigcap_{i} f(i) \] where $\mathrm{PLift.up}$ is the lifting function from $\iota$ to $\mathrm{PLift}\,\iota$.

Set.iInter_plift_down theorem

(f : ι → Set α) : ⋂ i, f (PLift.down i) = ⋂ i, f i

Full source

theorem iInter_plift_down (f : ι → Set α) : ⋂ i, f (PLift.down i) = ⋂ i, f i :=
  iInf_plift_down _

Intersection Invariance under PLift Projection

Informal description

For any family of sets $\{f(i)\}_{i \in \iota}$ indexed by a type $\iota$, the intersection $\bigcap_{i \in \iota} f(\mathrm{PLift.down}(i))$ is equal to $\bigcap_{i \in \iota} f(i)$, where $\mathrm{PLift.down}$ is the canonical projection from the lifted type.

Set.iUnion_eq_if theorem

{p : Prop} [Decidable p] (s : Set α) : ⋃ _ : p, s = if p then s else ∅

Full source

theorem iUnion_eq_if {p : Prop} [Decidable p] (s : Set α) : ⋃ _ : p, s = if p then s else ∅ :=
  iSup_eq_if _

Union over Proposition Conditionally Equals Set or Empty Set

Informal description

For any proposition $p$ with a decidability instance and any set $s$ of type $\alpha$, the union of $s$ over all proofs of $p$ is equal to $s$ if $p$ is true, and the empty set otherwise. That is, \[ \bigcup_{\_ : p} s = \begin{cases} s & \text{if } p \\ \emptyset & \text{otherwise} \end{cases} \]

Set.iUnion_eq_dif theorem

{p : Prop} [Decidable p] (s : p → Set α) : ⋃ h : p, s h = if h : p then s h else ∅

Full source

theorem iUnion_eq_dif {p : Prop} [Decidable p] (s : p → Set α) :
    ⋃ h : p, s h = if h : p then s h else ∅ :=
  iSup_eq_dif _

Union of Conditionally Indexed Sets Equals Conditional Expression

Informal description

For any proposition $p$ with a decidability instance, and for any family of sets $s$ indexed by proofs of $p$, the union $\bigcup_{h:p} s(h)$ equals $s(h)$ if $p$ holds (with proof $h$), and equals the empty set $\emptyset$ otherwise.

Set.iInter_eq_if theorem

{p : Prop} [Decidable p] (s : Set α) : ⋂ _ : p, s = if p then s else univ

Full source

theorem iInter_eq_if {p : Prop} [Decidable p] (s : Set α) : ⋂ _ : p, s = if p then s else univ :=
  iInf_eq_if _

Intersection over Proposition Conditionally Equals Set or Universe

Informal description

For any set $s$ in a type $\alpha$ and any decidable proposition $p$, the intersection $\bigcap_{h : p} s$ equals $s$ if $p$ is true, and equals the universal set $\text{univ}$ otherwise.

Set.iInf_eq_dif theorem

{p : Prop} [Decidable p] (s : p → Set α) : ⋂ h : p, s h = if h : p then s h else univ

Full source

theorem iInf_eq_dif {p : Prop} [Decidable p] (s : p → Set α) :
    ⋂ h : p, s h = if h : p then s h else univ :=
  _root_.iInf_eq_dif _

Conditional Intersection Equals If-Then-Else

Informal description

For any decidable proposition $p$ and any family of sets $s$ indexed by $p$, the intersection $\bigcap_{h : p} s(h)$ equals $s(h)$ if $p$ holds, and equals the universal set $\text{univ}$ otherwise.

Set.exists_set_mem_of_union_eq_top theorem

{ι : Type*} (t : Set ι) (s : ι → Set β) (w : ⋃ i ∈ t, s i = ⊤) (x : β) : ∃ i ∈ t, x ∈ s i

Full source

theorem exists_set_mem_of_union_eq_top {ι : Type*} (t : Set ι) (s : ι → Set β)
    (w : ⋃ i ∈ t, s i = ⊤) (x : β) : ∃ i ∈ t, x ∈ s i := by
  have p : x ∈ ⊤ := Set.mem_univ x
  rw [← w, Set.mem_iUnion] at p
  simpa using p

Existence of Index in Covering Union

Informal description

Let $t$ be a set of indices of type $\iota$, and let $s : \iota \to \text{Set } \beta$ be a family of sets indexed by $\iota$. If the union of all sets $s_i$ for $i \in t$ equals the universal set $\top$, then for every element $x \in \beta$, there exists an index $i \in t$ such that $x \in s_i$.

Set.nonempty_of_union_eq_top_of_nonempty theorem

{ι : Type*} (t : Set ι) (s : ι → Set α) (H : Nonempty α) (w : ⋃ i ∈ t, s i = ⊤) : t.Nonempty

Full source

theorem nonempty_of_union_eq_top_of_nonempty {ι : Type*} (t : Set ι) (s : ι → Set α)
    (H : Nonempty α) (w : ⋃ i ∈ t, s i = ⊤) : t.Nonempty := by
  obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
  exact ⟨x, m⟩

Nonempty Index Set from Covering Union of Nonempty Type

Informal description

Let $t$ be a set of indices of type $\iota$, and let $s : \iota \to \text{Set } \alpha$ be a family of sets indexed by $\iota$. If $\alpha$ is nonempty and the union $\bigcup_{i \in t} s_i$ equals the universal set $\top$, then the set of indices $t$ is nonempty.

Set.nonempty_of_nonempty_iUnion theorem

{s : ι → Set α} (h_Union : (⋃ i, s i).Nonempty) : Nonempty ι

Full source

theorem nonempty_of_nonempty_iUnion
    {s : ι → Set α} (h_Union : (⋃ i, s i).Nonempty) : Nonempty ι := by
  obtain ⟨x, hx⟩ := h_Union
  exact ⟨Classical.choose <| mem_iUnion.mp hx⟩

Nonempty Index Type from Nonempty Union of Sets

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$, if the union $\bigcup_{i} s_i$ is nonempty, then the index type $\iota$ is nonempty.

Set.nonempty_of_nonempty_iUnion_eq_univ theorem

{s : ι → Set α} [Nonempty α] (h_Union : ⋃ i, s i = univ) : Nonempty ι

Full source

theorem nonempty_of_nonempty_iUnion_eq_univ
    {s : ι → Set α} [Nonempty α] (h_Union : ⋃ i, s i = univ) : Nonempty ι :=
  nonempty_of_nonempty_iUnion (s := s) (by simpa only [h_Union] using univ_nonempty)

Nonempty Index Type from Covering Union of Nonempty Type

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ in a nonempty type $\alpha$, if the union $\bigcup_{i} s_i$ equals the universal set $\text{univ}$, then the index type $\iota$ is nonempty.

Set.setOf_exists theorem

(p : ι → β → Prop) : {x | ∃ i, p i x} = ⋃ i, {x | p i x}

Full source

theorem setOf_exists (p : ι → β → Prop) : { x | ∃ i, p i x } = ⋃ i, { x | p i x } :=
  ext fun _ => mem_iUnion.symm

Set Construction via Existential Quantifier Equals Union of Fibers

Informal description

For any family of predicates $p_i : \beta \to \text{Prop}$ indexed by $i \in \iota$, the set of elements $x \in \beta$ such that there exists an $i$ with $p_i(x)$ is equal to the union over all $i$ of the sets $\{x \mid p_i(x)\}$. In symbols: $$ \{x \mid \exists i, p_i(x)\} = \bigcup_{i} \{x \mid p_i(x)\}. $$

Set.setOf_forall theorem

(p : ι → β → Prop) : {x | ∀ i, p i x} = ⋂ i, {x | p i x}

Full source

theorem setOf_forall (p : ι → β → Prop) : { x | ∀ i, p i x } = ⋂ i, { x | p i x } :=
  ext fun _ => mem_iInter.symm

Universal Quantifier as Intersection of Sets

Informal description

For any family of predicates $p_i : \beta \to \text{Prop}$ indexed by $i \in \iota$, the set of all elements $x \in \beta$ satisfying $\forall i, p_i x$ is equal to the intersection over all $i$ of the sets $\{x \mid p_i x\}$. In symbols: $$ \{x \mid \forall i, p_i x\} = \bigcap_i \{x \mid p_i x\}. $$

Set.iUnion_subset theorem

{s : ι → Set α} {t : Set α} (h : ∀ i, s i ⊆ t) : ⋃ i, s i ⊆ t

Full source

theorem iUnion_subset {s : ι → Set α} {t : Set α} (h : ∀ i, s i ⊆ t) : ⋃ i, s i⋃ i, s i ⊆ t :=
  iSup_le h

Union Subset Property: $\bigcup_i s_i \subseteq t$ when each $s_i \subseteq t$

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ and a set $t$ in a type $\alpha$, if each $s_i$ is a subset of $t$, then the union $\bigcup_{i} s_i$ is also a subset of $t$.

Set.iUnion₂_subset theorem

{s : ∀ i, κ i → Set α} {t : Set α} (h : ∀ i j, s i j ⊆ t) : ⋃ (i) (j), s i j ⊆ t

Full source

theorem iUnion₂_subset {s : ∀ i, κ i → Set α} {t : Set α} (h : ∀ i j, s i j ⊆ t) :
    ⋃ (i) (j), s i j⋃ (i) (j), s i j ⊆ t :=
  iUnion_subset fun x => iUnion_subset (h x)

Double Union Subset Property: $\bigcup_{i,j} s_{i,j} \subseteq t$ when each $s_{i,j} \subseteq t$

Informal description

For any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ and a set $t$ in a type $\alpha$, if each $s_{i,j}$ is a subset of $t$, then the union $\bigcup_{i,j} s_{i,j}$ is also a subset of $t$.

Set.subset_iInter theorem

{t : Set β} {s : ι → Set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i

Full source

theorem subset_iInter {t : Set β} {s : ι → Set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=
  le_iInf h

Subset Preservation under Intersection of a Family of Sets

Informal description

For any set $t$ and any family of sets $\{s_i\}_{i \in \iota}$, if $t$ is a subset of $s_i$ for every index $i$, then $t$ is also a subset of the intersection $\bigcap_{i} s_i$.

Set.subset_iInter₂ theorem

{s : Set α} {t : ∀ i, κ i → Set α} (h : ∀ i j, s ⊆ t i j) : s ⊆ ⋂ (i) (j), t i j

Full source

theorem subset_iInter₂ {s : Set α} {t : ∀ i, κ i → Set α} (h : ∀ i j, s ⊆ t i j) :
    s ⊆ ⋂ (i) (j), t i j :=
  subset_iInter fun x => subset_iInter <| h x

Subset Preservation under Double Intersection of a Family of Sets

Informal description

For any set $s$ and any family of sets $\{t_{i,j}\}_{i,j}$ indexed by $i$ and $j$, if $s$ is a subset of $t_{i,j}$ for every pair of indices $i$ and $j$, then $s$ is also a subset of the intersection $\bigcap_{i,j} t_{i,j}$.

Set.iUnion_subset_iff theorem

{s : ι → Set α} {t : Set α} : ⋃ i, s i ⊆ t ↔ ∀ i, s i ⊆ t

Full source

@[simp]
theorem iUnion_subset_iff {s : ι → Set α} {t : Set α} : ⋃ i, s i⋃ i, s i ⊆ t⋃ i, s i ⊆ t ↔ ∀ i, s i ⊆ t :=
  ⟨fun h _ => Subset.trans (le_iSup s _) h, iUnion_subset⟩

Characterization of Union Subset via Pointwise Containment

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ and any set $t$ in a type $\alpha$, the union $\bigcup_{i} s_i$ is a subset of $t$ if and only if for every index $i$, the set $s_i$ is a subset of $t$.

Set.iUnion₂_subset_iff theorem

{s : ∀ i, κ i → Set α} {t : Set α} : ⋃ (i) (j), s i j ⊆ t ↔ ∀ i j, s i j ⊆ t

Full source

theorem iUnion₂_subset_iff {s : ∀ i, κ i → Set α} {t : Set α} :
    ⋃ (i) (j), s i j⋃ (i) (j), s i j ⊆ t⋃ (i) (j), s i j ⊆ t ↔ ∀ i j, s i j ⊆ t := by simp_rw [iUnion_subset_iff]

Union of Indexed Family Subset Equivalence

Informal description

For any family of sets $\{s_{i,j}\}_{i,j}$ indexed by $i$ and $j$, and any set $t$, the union $\bigcup_{i,j} s_{i,j}$ is a subset of $t$ if and only if every set $s_{i,j}$ in the family is a subset of $t$.

Set.subset_iInter_iff theorem

{s : Set α} {t : ι → Set α} : (s ⊆ ⋂ i, t i) ↔ ∀ i, s ⊆ t i

Full source

@[simp]
theorem subset_iInter_iff {s : Set α} {t : ι → Set α} : (s ⊆ ⋂ i, t i) ↔ ∀ i, s ⊆ t i :=
  le_iInf_iff

Characterization of Subset of Intersection via Pointwise Containment

Informal description

For any set $s$ and any family of sets $\{t_i\}_{i \in \iota}$, the set $s$ is contained in the intersection $\bigcap_{i} t_i$ if and only if for every index $i$, the set $s$ is contained in $t_i$.

Set.subset_iInter₂_iff theorem

{s : Set α} {t : ∀ i, κ i → Set α} : (s ⊆ ⋂ (i) (j), t i j) ↔ ∀ i j, s ⊆ t i j

Full source

theorem subset_iInter₂_iff {s : Set α} {t : ∀ i, κ i → Set α} :
    (s ⊆ ⋂ (i) (j), t i j) ↔ ∀ i j, s ⊆ t i j := by simp_rw [subset_iInter_iff]

Characterization of Subset of Double Intersection via Pointwise Containment

Informal description

For any set $s$ and any family of sets $\{t_{i,j}\}_{i,j}$ indexed by $i$ and $j$, the set $s$ is contained in the intersection $\bigcap_{i,j} t_{i,j}$ if and only if for every pair of indices $(i,j)$, the set $s$ is contained in $t_{i,j}$.

Set.subset_iUnion theorem

: ∀ (s : ι → Set β) (i : ι), s i ⊆ ⋃ i, s i

Full source

theorem subset_iUnion : ∀ (s : ι → Set β) (i : ι), s i ⊆ ⋃ i, s i :=
  le_iSup

Elementary Set Containment in Union: $s_i \subseteq \bigcup_i s_i$

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ indexed by $\iota$ and any index $i \in \iota$, the set $s_i$ is contained in the union $\bigcup_{i \in \iota} s_i$.

Set.iInter_subset theorem

: ∀ (s : ι → Set β) (i : ι), ⋂ i, s i ⊆ s i

Full source

theorem iInter_subset : ∀ (s : ι → Set β) (i : ι), ⋂ i, s i⋂ i, s i ⊆ s i :=
  iInf_le

Intersection is Subset of Each Set in Indexed Family

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\beta$, the intersection of all $s_i$ is contained in each individual set $s_i$, i.e., $\bigcap_{i \in \iota} s_i \subseteq s_i$ for every $i \in \iota$.

Set.iInter_subset_iUnion theorem

[Nonempty ι] {s : ι → Set α} : ⋂ i, s i ⊆ ⋃ i, s i

Full source

lemma iInter_subset_iUnion [Nonempty ι] {s : ι → Set α} : ⋂ i, s i⋂ i, s i ⊆ ⋃ i, s i := iInf_le_iSup

Intersection is Subset of Union for Nonempty Indexed Family of Sets

Informal description

For any nonempty index type $\iota$ and any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, the intersection of all $s_i$ is contained in their union, i.e., $\bigcap_{i \in \iota} s_i \subseteq \bigcup_{i \in \iota} s_i$.

Set.subset_iUnion₂ theorem

{s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : s i j ⊆ ⋃ (i') (j'), s i' j'

Full source

theorem subset_iUnion₂ {s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : s i j ⊆ ⋃ (i') (j'), s i' j' :=
  le_iSup₂ i j

Inclusion of Set in Double-Indexed Union

Informal description

For any indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, and for any specific indices $i \in \iota$ and $j \in \kappa_i$, the set $s_{i,j}$ is contained in the union of all sets in the family, i.e., $s_{i,j} \subseteq \bigcup_{i' \in \iota} \bigcup_{j' \in \kappa_{i'}} s_{i',j'}$.

Set.iInter₂_subset theorem

{s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : ⋂ (i) (j), s i j ⊆ s i j

Full source

theorem iInter₂_subset {s : ∀ i, κ i → Set α} (i : ι) (j : κ i) : ⋂ (i) (j), s i j⋂ (i) (j), s i j ⊆ s i j :=
  iInf₂_le i j

Double Intersection is Subset of Each Member Set

Informal description

For any indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, the intersection $\bigcap_{i,j} s_{i,j}$ is contained in each individual set $s_{i,j}$ for any given $i \in \iota$ and $j \in \kappa_i$.

Set.subset_iUnion_of_subset theorem

{s : Set α} {t : ι → Set α} (i : ι) (h : s ⊆ t i) : s ⊆ ⋃ i, t i

Full source

/-- This rather trivial consequence of `subset_iUnion`is convenient with `apply`, and has `i`
explicit for this purpose. -/
theorem subset_iUnion_of_subset {s : Set α} {t : ι → Set α} (i : ι) (h : s ⊆ t i) : s ⊆ ⋃ i, t i :=
  le_iSup_of_le i h

Subset Preservation Under Union Inclusion

Informal description

For any set $s$ and any indexed family of sets $t_i$ (where $i$ ranges over some index set), if $s$ is a subset of $t_i$ for some particular index $i$, then $s$ is also a subset of the union $\bigcup_i t_i$.

Set.iInter_subset_of_subset theorem

{s : ι → Set α} {t : Set α} (i : ι) (h : s i ⊆ t) : ⋂ i, s i ⊆ t

Full source

/-- This rather trivial consequence of `iInter_subset`is convenient with `apply`, and has `i`
explicit for this purpose. -/
theorem iInter_subset_of_subset {s : ι → Set α} {t : Set α} (i : ι) (h : s i ⊆ t) :
    ⋂ i, s i⋂ i, s i ⊆ t :=
  iInf_le_of_le i h

Intersection Subset Property: $\bigcap_i s_i \subseteq t$ when $s_i \subseteq t$ for some $i$

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any set $t \subseteq \alpha$, if there exists an index $i \in \iota$ such that $s_i \subseteq t$, then the intersection $\bigcap_{i \in \iota} s_i$ is also a subset of $t$.

Set.subset_iUnion₂_of_subset theorem

{s : Set α} {t : ∀ i, κ i → Set α} (i : ι) (j : κ i) (h : s ⊆ t i j) : s ⊆ ⋃ (i) (j), t i j

Full source

/-- This rather trivial consequence of `subset_iUnion₂` is convenient with `apply`, and has `i` and
`j` explicit for this purpose. -/
theorem subset_iUnion₂_of_subset {s : Set α} {t : ∀ i, κ i → Set α} (i : ι) (j : κ i)
    (h : s ⊆ t i j) : s ⊆ ⋃ (i) (j), t i j :=
  le_iSup₂_of_le i j h

Subset of Union from Subset of Indexed Family Member

Informal description

For any set $s$ and any indexed family of sets $t_i$ (where $i \in \iota$ and $j \in \kappa_i$), if $s$ is a subset of $t_i(j)$ for some specific $i$ and $j$, then $s$ is also a subset of the union $\bigcup_{i,j} t_i(j)$.

Set.iInter₂_subset_of_subset theorem

{s : ∀ i, κ i → Set α} {t : Set α} (i : ι) (j : κ i) (h : s i j ⊆ t) : ⋂ (i) (j), s i j ⊆ t

Full source

/-- This rather trivial consequence of `iInter₂_subset` is convenient with `apply`, and has `i` and
`j` explicit for this purpose. -/
theorem iInter₂_subset_of_subset {s : ∀ i, κ i → Set α} {t : Set α} (i : ι) (j : κ i)
    (h : s i j ⊆ t) : ⋂ (i) (j), s i j⋂ (i) (j), s i j ⊆ t :=
  iInf₂_le_of_le i j h

Intersection Subset Property for Indexed Family of Sets

Informal description

For any family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ and any set $t$, if there exist indices $i \in \iota$ and $j \in \kappa_i$ such that $s_{i,j} \subseteq t$, then the intersection $\bigcap_{i,j} s_{i,j}$ is a subset of $t$.

Set.iUnion_mono theorem

{s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : ⋃ i, s i ⊆ ⋃ i, t i

Full source

theorem iUnion_mono {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : ⋃ i, s i⋃ i, s i ⊆ ⋃ i, t i :=
  iSup_mono h

Monotonicity of Union over Indexed Family of Sets

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, if $s_i \subseteq t_i$ for every index $i$, then the union of all $s_i$ is contained in the union of all $t_i$, i.e., $$\bigcup_{i} s_i \subseteq \bigcup_{i} t_i.$$

Set.iUnion_mono'' theorem

{s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : iUnion s ⊆ iUnion t

Full source

@[gcongr]
theorem iUnion_mono'' {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : iUnioniUnion s ⊆ iUnion t :=
  iSup_mono h

Monotonicity of Union over Indexed Family of Sets

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, if $s_i \subseteq t_i$ for every index $i$, then the union of all $s_i$ is contained in the union of all $t_i$, i.e., $$\bigcup_{i} s_i \subseteq \bigcup_{i} t_i.$$

Set.iUnion₂_mono theorem

{s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j ⊆ t i j) : ⋃ (i) (j), s i j ⊆ ⋃ (i) (j), t i j

Full source

theorem iUnion₂_mono {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j ⊆ t i j) :
    ⋃ (i) (j), s i j⋃ (i) (j), s i j ⊆ ⋃ (i) (j), t i j :=
  iSup₂_mono h

Monotonicity of Double Union over Indexed Family of Sets

Informal description

For any doubly indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ and $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if $s_{i,j} \subseteq t_{i,j}$ for every index $i$ and $j$, then the union of all $s_{i,j}$ is contained in the union of all $t_{i,j}$, i.e., $$\bigcup_{i,j} s_{i,j} \subseteq \bigcup_{i,j} t_{i,j}.$$

Set.iInter_mono theorem

{s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : ⋂ i, s i ⊆ ⋂ i, t i

Full source

theorem iInter_mono {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : ⋂ i, s i⋂ i, s i ⊆ ⋂ i, t i :=
  iInf_mono h

Monotonicity of Intersection with Respect to Inclusion

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, if $s_i \subseteq t_i$ for every $i \in \iota$, then the intersection of all $s_i$ is contained in the intersection of all $t_i$, i.e., \[ \bigcap_{i \in \iota} s_i \subseteq \bigcap_{i \in \iota} t_i. \]

Set.iInter_mono'' theorem

{s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : iInter s ⊆ iInter t

Full source

@[gcongr]
theorem iInter_mono'' {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : iInteriInter s ⊆ iInter t :=
  iInf_mono h

Monotonicity of Indexed Intersection with Respect to Set Inclusion

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, if $s_i \subseteq t_i$ for all $i \in \iota$, then the intersection of all $s_i$ is contained in the intersection of all $t_i$, i.e., $\bigcap_{i} s_i \subseteq \bigcap_{i} t_i$.

Set.iInter₂_mono theorem

{s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j ⊆ t i j) : ⋂ (i) (j), s i j ⊆ ⋂ (i) (j), t i j

Full source

theorem iInter₂_mono {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j ⊆ t i j) :
    ⋂ (i) (j), s i j⋂ (i) (j), s i j ⊆ ⋂ (i) (j), t i j :=
  iInf₂_mono h

Monotonicity of Double Intersection with Respect to Inclusion

Informal description

For any indexed family of sets $\{s_{i,j}\}_{i,j}$ and $\{t_{i,j}\}_{i,j}$ in a type $\alpha$, if for every $i$ and $j$ we have $s_{i,j} \subseteq t_{i,j}$, then the intersection $\bigcap_{i,j} s_{i,j}$ is contained in the intersection $\bigcap_{i,j} t_{i,j}$.

Set.iUnion_mono' theorem

{s : ι → Set α} {t : ι₂ → Set α} (h : ∀ i, ∃ j, s i ⊆ t j) : ⋃ i, s i ⊆ ⋃ i, t i

Full source

theorem iUnion_mono' {s : ι → Set α} {t : ι₂ → Set α} (h : ∀ i, ∃ j, s i ⊆ t j) :
    ⋃ i, s i⋃ i, s i ⊆ ⋃ i, t i :=
  iSup_mono' h

Union Monotonicity under Pointwise Containment

Informal description

Let $\{s_i\}_{i \in I}$ and $\{t_j\}_{j \in J}$ be two families of subsets of a set $\alpha$. If for every $i \in I$ there exists $j \in J$ such that $s_i \subseteq t_j$, then the union of all $s_i$ is contained in the union of all $t_j$, i.e., \[ \bigcup_{i \in I} s_i \subseteq \bigcup_{j \in J} t_j. \]

Set.iUnion₂_mono' theorem

 {s : ∀ i, κ i → Set α} {t : ∀ i', κ' i' → Set α} (h : ∀ i j, ∃ i' j', s i j ⊆ t i' j') :
  ⋃ (i) (j), s i j ⊆ ⋃ (i') (j'), t i' j'

Full source

theorem iUnion₂_mono' {s : ∀ i, κ i → Set α} {t : ∀ i', κ' i' → Set α}
    (h : ∀ i j, ∃ i' j', s i j ⊆ t i' j') : ⋃ (i) (j), s i j⋃ (i) (j), s i j ⊆ ⋃ (i') (j'), t i' j' :=
  iSup₂_mono' h

Monotonicity of Double Union Under Componentwise Containment

Informal description

Let $\{s_{i,j}\}_{i,j}$ and $\{t_{i',j'}\}_{i',j'}$ be two doubly-indexed families of sets in a type $\alpha$. If for every pair $(i,j)$ there exists a pair $(i',j')$ such that $s_{i,j} \subseteq t_{i',j'}$, then the union of all $s_{i,j}$ is contained in the union of all $t_{i',j'}$. That is, \[ \bigcup_{i,j} s_{i,j} \subseteq \bigcup_{i',j'} t_{i',j'}. \]

Set.iInter_mono' theorem

{s : ι → Set α} {t : ι' → Set α} (h : ∀ j, ∃ i, s i ⊆ t j) : ⋂ i, s i ⊆ ⋂ j, t j

Full source

theorem iInter_mono' {s : ι → Set α} {t : ι' → Set α} (h : ∀ j, ∃ i, s i ⊆ t j) :
    ⋂ i, s i⋂ i, s i ⊆ ⋂ j, t j :=
  Set.subset_iInter fun j =>
    let ⟨i, hi⟩ := h j
    iInter_subset_of_subset i hi

Monotonicity of Intersection Under Componentwise Containment

Informal description

For any two indexed families of sets $\{s_i\}_{i \in \iota}$ and $\{t_j\}_{j \in \iota'}$ in a type $\alpha$, if for every index $j \in \iota'$ there exists an index $i \in \iota$ such that $s_i \subseteq t_j$, then the intersection $\bigcap_{i \in \iota} s_i$ is contained in the intersection $\bigcap_{j \in \iota'} t_j$.

Set.iInter₂_mono' theorem

 {s : ∀ i, κ i → Set α} {t : ∀ i', κ' i' → Set α} (h : ∀ i' j', ∃ i j, s i j ⊆ t i' j') :
  ⋂ (i) (j), s i j ⊆ ⋂ (i') (j'), t i' j'

Full source

theorem iInter₂_mono' {s : ∀ i, κ i → Set α} {t : ∀ i', κ' i' → Set α}
    (h : ∀ i' j', ∃ i j, s i j ⊆ t i' j') : ⋂ (i) (j), s i j⋂ (i) (j), s i j ⊆ ⋂ (i') (j'), t i' j' :=
  subset_iInter₂_iff.2 fun i' j' =>
    let ⟨_, _, hst⟩ := h i' j'
    (iInter₂_subset _ _).trans hst

Monotonicity of Double Intersection Under Componentwise Containment

Informal description

Let $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ and $\{t_{i',j'}\}_{i' \in \iota', j' \in \kappa'_{i'}}$ be two doubly-indexed families of sets in a type $\alpha$. If for every pair $(i',j')$ there exists a pair $(i,j)$ such that $s_{i,j} \subseteq t_{i',j'}$, then the intersection of all $s_{i,j}$ is contained in the intersection of all $t_{i',j'}$. That is, \[ \bigcap_{i,j} s_{i,j} \subseteq \bigcap_{i',j'} t_{i',j'}. \]

Set.iUnion₂_subset_iUnion theorem

(κ : ι → Sort*) (s : ι → Set α) : ⋃ (i) (_ : κ i), s i ⊆ ⋃ i, s i

Full source

theorem iUnion₂_subset_iUnion (κ : ι → Sort*) (s : ι → Set α) :
    ⋃ (i) (_ : κ i), s i⋃ (i) (_ : κ i), s i ⊆ ⋃ i, s i :=
  iUnion_mono fun _ => iUnion_subset fun _ => Subset.rfl

Union over Double Index is Contained in Union over Single Index

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any family of types $\kappa_i$ indexed by $i \in \iota$, the union $\bigcup_{i \in \iota, j \in \kappa_i} s_i$ is contained in the union $\bigcup_{i \in \iota} s_i$. In symbols: \[ \bigcup_{i \in \iota, j \in \kappa_i} s_i \subseteq \bigcup_{i \in \iota} s_i \]

Set.iInter_subset_iInter₂ theorem

(κ : ι → Sort*) (s : ι → Set α) : ⋂ i, s i ⊆ ⋂ (i) (_ : κ i), s i

Full source

theorem iInter_subset_iInter₂ (κ : ι → Sort*) (s : ι → Set α) :
    ⋂ i, s i⋂ i, s i ⊆ ⋂ (i) (_ : κ i), s i :=
  iInter_mono fun _ => subset_iInter fun _ => Subset.rfl

Intersection is Contained in Double Intersection

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$, and any family of types $\kappa_i$ for each $i \in \iota$, the intersection $\bigcap_{i} s_i$ is contained in the double intersection $\bigcap_{i} \bigcap_{j \in \kappa_i} s_i$. In symbols: \[ \bigcap_{i \in \iota} s_i \subseteq \bigcap_{i \in \iota} \bigcap_{j \in \kappa_i} s_i \]

Set.iUnion_setOf theorem

(P : ι → α → Prop) : ⋃ i, {x : α | P i x} = {x : α | ∃ i, P i x}

Full source

theorem iUnion_setOf (P : ι → α → Prop) : ⋃ i, { x : α | P i x } = { x : α | ∃ i, P i x } := by
  ext
  exact mem_iUnion

Union of Sets Defined by Predicates Equals Set Defined by Existential Predicate

Informal description

For any family of predicates $P_i : \alpha \to \text{Prop}$ indexed by $i \in \iota$, the union of the sets $\{x \in \alpha \mid P_i(x)\}$ over all $i$ is equal to the set $\{x \in \alpha \mid \exists i, P_i(x)\}$. In symbols: \[ \bigcup_{i \in \iota} \{x \in \alpha \mid P_i(x)\} = \{x \in \alpha \mid \exists i \in \iota, P_i(x)\} \]

Set.iInter_setOf theorem

(P : ι → α → Prop) : ⋂ i, {x : α | P i x} = {x : α | ∀ i, P i x}

Full source

theorem iInter_setOf (P : ι → α → Prop) : ⋂ i, { x : α | P i x } = { x : α | ∀ i, P i x } := by
  ext
  exact mem_iInter

Intersection of Predicate Sets Equals Universal Predicate Set

Informal description

For any family of predicates $P_i : \alpha \to \text{Prop}$ indexed by $i \in \iota$, the intersection of the sets $\{x \in \alpha \mid P_i x\}$ over all $i$ is equal to the set $\{x \in \alpha \mid \forall i, P_i x\}$. In symbols: \[ \bigcap_{i} \{x \mid P_i x\} = \{x \mid \forall i, P_i x\} \]

Set.iUnion_congr_of_surjective theorem

 {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Surjective h) (h2 : ∀ x, g (h x) = f x) : ⋃ x, f x = ⋃ y, g y

Full source

theorem iUnion_congr_of_surjective {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Surjective h)
    (h2 : ∀ x, g (h x) = f x) : ⋃ x, f x = ⋃ y, g y :=
  h1.iSup_congr h h2

Equality of Unions under Surjective Index Remapping

Informal description

Let $f : \iota \to \mathcal{P}(\alpha)$ and $g : \iota_2 \to \mathcal{P}(\alpha)$ be families of sets, and let $h : \iota \to \iota_2$ be a surjective function such that for all $x \in \iota$, $g(h(x)) = f(x)$. Then the union of the sets in the family $f$ equals the union of the sets in the family $g$, i.e., \[ \bigcup_{x \in \iota} f(x) = \bigcup_{y \in \iota_2} g(y). \]

Set.iInter_congr_of_surjective theorem

 {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Surjective h) (h2 : ∀ x, g (h x) = f x) : ⋂ x, f x = ⋂ y, g y

Full source

theorem iInter_congr_of_surjective {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Surjective h)
    (h2 : ∀ x, g (h x) = f x) : ⋂ x, f x = ⋂ y, g y :=
  h1.iInf_congr h h2

Intersection Equality under Surjective Index Transformation

Informal description

Let $f : \iota \to \text{Set } \alpha$ and $g : \iota_2 \to \text{Set } \alpha$ be indexed families of sets, and let $h : \iota \to \iota_2$ be a surjective function such that $g(h(x)) = f(x)$ for all $x \in \iota$. Then the intersection of all sets in the family $f$ equals the intersection of all sets in the family $g$, i.e., \[ \bigcap_{x \in \iota} f(x) = \bigcap_{y \in \iota_2} g(y). \]

Set.iUnion_congr theorem

{s t : ι → Set α} (h : ∀ i, s i = t i) : ⋃ i, s i = ⋃ i, t i

Full source

lemma iUnion_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : ⋃ i, s i = ⋃ i, t i := iSup_congr h

Equality of Unions under Pointwise Equality of Families

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, if $s_i = t_i$ for every index $i$, then their unions are equal, i.e., $\bigcup_{i} s_i = \bigcup_{i} t_i$.

Set.iInter_congr theorem

{s t : ι → Set α} (h : ∀ i, s i = t i) : ⋂ i, s i = ⋂ i, t i

Full source

lemma iInter_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : ⋂ i, s i = ⋂ i, t i := iInf_congr h

Equality of Indexed Families Implies Equality of Their Intersections

Informal description

For any indexed families of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, if $s_i = t_i$ for every index $i$, then the intersection of all $s_i$ equals the intersection of all $t_i$, i.e., $\bigcap_{i} s_i = \bigcap_{i} t_i$.

Set.iUnion₂_congr theorem

{s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) : ⋃ (i) (j), s i j = ⋃ (i) (j), t i j

Full source

lemma iUnion₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) :
    ⋃ (i) (j), s i j = ⋃ (i) (j), t i j :=
  iUnion_congr fun i => iUnion_congr <| h i

Equality of Double Unions under Pointwise Equality of Families

Informal description

For any indexed families of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ and $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if $s_{i,j} = t_{i,j}$ for every index $i$ and $j$, then their double unions are equal, i.e., $\bigcup_{i} \bigcup_{j} s_{i,j} = \bigcup_{i} \bigcup_{j} t_{i,j}$.

Set.iInter₂_congr theorem

{s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) : ⋂ (i) (j), s i j = ⋂ (i) (j), t i j

Full source

lemma iInter₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) :
    ⋂ (i) (j), s i j = ⋂ (i) (j), t i j :=
  iInter_congr fun i => iInter_congr <| h i

Equality of Doubly Indexed Families Implies Equality of Their Double Intersections

Informal description

For any doubly indexed families of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ and $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, if $s_{i,j} = t_{i,j}$ for every index $i$ and $j$, then the intersection of all $s_{i,j}$ equals the intersection of all $t_{i,j}$, i.e., $\bigcap_{i} \bigcap_{j} s_{i,j} = \bigcap_{i} \bigcap_{j} t_{i,j}$.

Set.iUnion_const theorem

(s : Set β) : ⋃ _ : ι, s = s

Full source

lemma iUnion_const (s : Set β) : ⋃ _ : ι, s = s := iSup_const

Union of a Constant Set over Any Index Type

Informal description

For any set $s$ in a type $\beta$, the union of $s$ over an arbitrary index type $\iota$ is equal to $s$ itself, i.e., $\bigcup_{i \in \iota} s = s$.

Set.iInter_const theorem

(s : Set β) : ⋂ _ : ι, s = s

Full source

lemma iInter_const (s : Set β) : ⋂ _ : ι, s = s := iInf_const

Intersection over Arbitrary Index Type is Identity

Informal description

For any set $s$ in a type $\beta$, the intersection of $s$ over an arbitrary index type $\iota$ is equal to $s$ itself, i.e., $\bigcap_{i \in \iota} s = s$.

Set.iUnion_eq_const theorem

(hf : ∀ i, f i = s) : ⋃ i, f i = s

Full source

lemma iUnion_eq_const (hf : ∀ i, f i = s) : ⋃ i, f i = s :=
  (iUnion_congr hf).trans <| iUnion_const _

Union of Constant Family Equals Constant Set

Informal description

For any indexed family of sets $\{f_i\}_{i \in \iota}$ in a type $\alpha$ and a fixed set $s \subseteq \alpha$, if $f_i = s$ for every index $i$, then the union of the family equals $s$, i.e., $\bigcup_{i} f_i = s$.

Set.iInter_eq_const theorem

(hf : ∀ i, f i = s) : ⋂ i, f i = s

Full source

lemma iInter_eq_const (hf : ∀ i, f i = s) : ⋂ i, f i = s :=
  (iInter_congr hf).trans <| iInter_const _

Intersection of Constant Indexed Family Equals the Constant Set

Informal description

For any indexed family of sets $\{f_i\}_{i \in \iota}$ and a set $s$ in a type $\alpha$, if $f_i = s$ for every index $i$, then the intersection of all $f_i$ equals $s$, i.e., $\bigcap_{i} f_i = s$.

Set.compl_iUnion theorem

(s : ι → Set β) : (⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ

Full source

@[simp]
theorem compl_iUnion (s : ι → Set β) : (⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ :=
  compl_iSup

De Morgan's Law for Complements of Indexed Unions

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\beta$, the complement of their union equals the intersection of their complements, i.e., $$ \left(\bigcup_{i} s_i\right)^c = \bigcap_{i} s_i^c. $$

Set.compl_iUnion₂ theorem

(s : ∀ i, κ i → Set α) : (⋃ (i) (j), s i j)ᶜ = ⋂ (i) (j), (s i j)ᶜ

Full source

theorem compl_iUnion₂ (s : ∀ i, κ i → Set α) : (⋃ (i) (j), s i j)ᶜ = ⋂ (i) (j), (s i j)ᶜ := by
  simp_rw [compl_iUnion]

De Morgan's Law for Complements of Doubly Indexed Unions

Informal description

For any doubly indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, the complement of their union equals the intersection of their complements, i.e., $$ \left(\bigcup_{i,j} s_{i,j}\right)^c = \bigcap_{i,j} s_{i,j}^c. $$

Set.compl_iInter theorem

(s : ι → Set β) : (⋂ i, s i)ᶜ = ⋃ i, (s i)ᶜ

Full source

@[simp]
theorem compl_iInter (s : ι → Set β) : (⋂ i, s i)ᶜ = ⋃ i, (s i)ᶜ :=
  compl_iInf

De Morgan's Law for Complements of Indexed Intersections

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\beta$, the complement of their intersection equals the union of their complements, i.e., $$ \left(\bigcap_{i} s_i\right)^c = \bigcup_{i} s_i^c. $$

Set.compl_iInter₂ theorem

(s : ∀ i, κ i → Set α) : (⋂ (i) (j), s i j)ᶜ = ⋃ (i) (j), (s i j)ᶜ

Full source

theorem compl_iInter₂ (s : ∀ i, κ i → Set α) : (⋂ (i) (j), s i j)ᶜ = ⋃ (i) (j), (s i j)ᶜ := by
  simp_rw [compl_iInter]

De Morgan's Law for Complements of Doubly Indexed Intersections

Informal description

For any doubly indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$, the complement of their intersection equals the union of their complements, i.e., $$ \left(\bigcap_{i} \bigcap_{j} s_{i,j}\right)^c = \bigcup_{i} \bigcup_{j} s_{i,j}^c. $$

Set.iUnion_eq_compl_iInter_compl theorem

(s : ι → Set β) : ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ

Full source

theorem iUnion_eq_compl_iInter_compl (s : ι → Set β) : ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ := by
  simp only [compl_iInter, compl_compl]

Union as Complement of Intersection of Complements

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\beta$, the union of the sets equals the complement of the intersection of their complements, i.e., $$ \bigcup_{i} s_i = \left(\bigcap_{i} s_i^c\right)^c. $$

Set.iInter_eq_compl_iUnion_compl theorem

(s : ι → Set β) : ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ

Full source

theorem iInter_eq_compl_iUnion_compl (s : ι → Set β) : ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ := by
  simp only [compl_iUnion, compl_compl]

Intersection as Complement of Union of Complements

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a type $\beta$, the intersection of the sets equals the complement of the union of their complements, i.e., $$ \bigcap_{i} s_i = \left( \bigcup_{i} s_i^c \right)^c. $$

Set.inter_iUnion theorem

(s : Set β) (t : ι → Set β) : (s ∩ ⋃ i, t i) = ⋃ i, s ∩ t i

Full source

theorem inter_iUnion (s : Set β) (t : ι → Set β) : (s ∩ ⋃ i, t i) = ⋃ i, s ∩ t i :=
  inf_iSup_eq _ _

Distributivity of Intersection over Union of Sets

Informal description

For any set $s$ in a type $\beta$ and any family of sets $\{t_i\}_{i \in \iota}$ indexed by $\iota$ in $\beta$, the intersection of $s$ with the union of the $t_i$ equals the union of the intersections of $s$ with each $t_i$. In symbols: $$ s \cap \left( \bigcup_{i} t_i \right) = \bigcup_{i} (s \cap t_i). $$

Set.iUnion_inter theorem

(s : Set β) (t : ι → Set β) : (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s

Full source

theorem iUnion_inter (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
  iSup_inf_eq _ _

Distributivity of Union over Intersection of Sets

Informal description

For any set $s$ in a type $\beta$ and any family of sets $\{t_i\}_{i \in \iota}$ indexed by $\iota$ in $\beta$, the intersection of the union of the $t_i$ with $s$ equals the union of the intersections of each $t_i$ with $s$. In symbols: $$ \left( \bigcup_{i} t_i \right) \cap s = \bigcup_{i} (t_i \cap s). $$

Set.iUnion_union_distrib theorem

(s : ι → Set β) (t : ι → Set β) : ⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i

Full source

theorem iUnion_union_distrib (s : ι → Set β) (t : ι → Set β) :
    ⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i :=
  iSup_sup_eq

Distributivity of Union over Indexed Union of Sets

Informal description

For any indexed families of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\beta$, the union of the pairwise unions $s_i \cup t_i$ equals the union of all $s_i$ combined with the union of all $t_i$. In symbols: $$ \bigcup_{i} (s_i \cup t_i) = \left( \bigcup_{i} s_i \right) \cup \left( \bigcup_{i} t_i \right). $$

Set.iInter_inter_distrib theorem

(s : ι → Set β) (t : ι → Set β) : ⋂ i, s i ∩ t i = (⋂ i, s i) ∩ ⋂ i, t i

Full source

theorem iInter_inter_distrib (s : ι → Set β) (t : ι → Set β) :
    ⋂ i, s i ∩ t i = (⋂ i, s i) ∩ ⋂ i, t i :=
  iInf_inf_eq

Distributivity of Indexed Intersection over Pairwise Intersection

Informal description

For any indexed family of sets $(s_i)_{i \in \iota}$ and $(t_i)_{i \in \iota}$ in a type $\beta$, the intersection of the pairwise intersections equals the intersection of the total intersections: \[ \bigcap_{i} (s_i \cap t_i) = \left(\bigcap_{i} s_i\right) \cap \left(\bigcap_{i} t_i\right) \]

Set.union_iUnion theorem

[Nonempty ι] (s : Set β) (t : ι → Set β) : (s ∪ ⋃ i, t i) = ⋃ i, s ∪ t i

Full source

theorem union_iUnion [Nonempty ι] (s : Set β) (t : ι → Set β) : (s ∪ ⋃ i, t i) = ⋃ i, s ∪ t i :=
  sup_iSup

Distributivity of Union over Indexed Union: $s \cup (\bigcup_i t_i) = \bigcup_i (s \cup t_i)$

Informal description

For a nonempty index type $\iota$ and any set $s$ in $\beta$, the union of $s$ with the union of a family of sets $\{t_i\}_{i \in \iota}$ is equal to the union over $\iota$ of $s$ union with each $t_i$. In symbols: $$ s \cup \left(\bigcup_{i \in \iota} t_i\right) = \bigcup_{i \in \iota} (s \cup t_i) $$

Set.iUnion_union theorem

[Nonempty ι] (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s

Full source

theorem iUnion_union [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
  iSup_sup

Distributivity of Union over Indexed Union: $(\bigcup_i t_i) \cup s = \bigcup_i (t_i \cup s)$

Informal description

For a nonempty index type $\iota$ and any set $s$ in $\beta$, the union of the indexed union $\bigcup_i t_i$ with $s$ equals the indexed union of the pairwise unions $\bigcup_i (t_i \cup s)$, where $t : \iota \to \text{Set} \beta$ is a family of sets indexed by $\iota$.

Set.inter_iInter theorem

[Nonempty ι] (s : Set β) (t : ι → Set β) : (s ∩ ⋂ i, t i) = ⋂ i, s ∩ t i

Full source

theorem inter_iInter [Nonempty ι] (s : Set β) (t : ι → Set β) : (s ∩ ⋂ i, t i) = ⋂ i, s ∩ t i :=
  inf_iInf

Intersection Distributes over Indexed Intersection

Informal description

For any nonempty index type $\iota$ and any set $s$ in a type $\beta$, and any family of sets $t_i$ indexed by $\iota$, the intersection of $s$ with the intersection of all $t_i$ is equal to the intersection over all $i$ of $s$ intersected with $t_i$. In symbols: $$ s \cap \bigcap_{i} t_i = \bigcap_{i} (s \cap t_i). $$

Set.iInter_inter theorem

[Nonempty ι] (s : Set β) (t : ι → Set β) : (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s

Full source

theorem iInter_inter [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
  iInf_inf

Intersection Distributes Over Indexed Intersection

Informal description

For a nonempty index type $\iota$ and any set $s$ in a type $\beta$, the intersection of the family of sets $\{t_i\}_{i \in \iota}$ with $s$ is equal to the intersection of the family $\{t_i \cap s\}_{i \in \iota}$. In other words: $$ \left(\bigcap_{i \in \iota} t_i\right) \cap s = \bigcap_{i \in \iota} (t_i \cap s) $$

Set.insert_iUnion theorem

[Nonempty ι] (x : β) (t : ι → Set β) : insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Full source

theorem insert_iUnion [Nonempty ι] (x : β) (t : ι → Set β) :
    insert x (⋃ i, t i) = ⋃ i, insert x (t i) := by
  simp_rw [← union_singleton, iUnion_union]

Insertion Distributes over Indexed Union: $\{x\} \cup \bigcup_i t_i = \bigcup_i (\{x\} \cup t_i)$

Informal description

For a nonempty index type $\iota$, an element $x$ of type $\beta$, and a family of sets $t_i$ indexed by $\iota$, the insertion of $x$ into the union $\bigcup_i t_i$ is equal to the union of the insertions of $x$ into each $t_i$. In symbols: $$ \{x\} \cup \left( \bigcup_{i} t_i \right) = \bigcup_{i} \left( \{x\} \cup t_i \right). $$

Set.union_iInter theorem

(s : Set β) (t : ι → Set β) : (s ∪ ⋂ i, t i) = ⋂ i, s ∪ t i

Full source

theorem union_iInter (s : Set β) (t : ι → Set β) : (s ∪ ⋂ i, t i) = ⋂ i, s ∪ t i :=
  sup_iInf_eq _ _

Distributivity of Union over Intersection

Informal description

For any set $s$ and any family of sets $\{t_i\}_{i \in \iota}$, the union of $s$ with the intersection of all $t_i$ is equal to the intersection of all unions $s \cup t_i$. That is, $$ s \cup \left( \bigcap_{i} t_i \right) = \bigcap_{i} (s \cup t_i). $$

Set.iInter_union theorem

(s : ι → Set β) (t : Set β) : (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t

Full source

theorem iInter_union (s : ι → Set β) (t : Set β) : (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t :=
  iInf_sup_eq _ _

Distributivity of Union over Intersection for Indexed Family of Sets

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ and any set $t$, the union of the intersection of all $s_i$ with $t$ equals the intersection of the unions of each $s_i$ with $t$. In symbols: $$\left(\bigcap_{i} s_i\right) \cup t = \bigcap_{i} (s_i \cup t)$$

Set.insert_iInter theorem

(x : β) (t : ι → Set β) : insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Full source

theorem insert_iInter (x : β) (t : ι → Set β) : insert x (⋂ i, t i) = ⋂ i, insert x (t i) := by
  simp_rw [← union_singleton, iInter_union]

Insertion Distributes over Intersection: $\{x\} \cup \bigcap_i t_i = \bigcap_i (\{x\} \cup t_i)$

Informal description

For any element $x$ of type $\beta$ and any family of sets $\{t_i\}_{i \in \iota}$ in $\beta$, the insertion of $x$ into the intersection of all $t_i$ equals the intersection of the insertions of $x$ into each $t_i$. In symbols: $$\{x\} \cup \left(\bigcap_{i} t_i\right) = \bigcap_{i} \left(\{x\} \cup t_i\right)$$

Set.iUnion_diff theorem

(s : Set β) (t : ι → Set β) : (⋃ i, t i) \ s = ⋃ i, t i \ s

Full source

theorem iUnion_diff (s : Set β) (t : ι → Set β) : (⋃ i, t i) \ s = ⋃ i, t i \ s :=
  iUnion_inter _ _

Distributivity of Set Difference over Union of Indexed Family

Informal description

For any set $s$ in a type $\beta$ and any family of sets $\{t_i\}_{i \in \iota}$ indexed by $\iota$ in $\beta$, the set difference between the union of the $t_i$ and $s$ equals the union of the set differences between each $t_i$ and $s$. In symbols: $$ \left( \bigcup_{i} t_i \right) \setminus s = \bigcup_{i} (t_i \setminus s). $$

Set.diff_iUnion theorem

[Nonempty ι] (s : Set β) (t : ι → Set β) : (s \ ⋃ i, t i) = ⋂ i, s \ t i

Full source

theorem diff_iUnion [Nonempty ι] (s : Set β) (t : ι → Set β) : (s \ ⋃ i, t i) = ⋂ i, s \ t i := by
  rw [diff_eq, compl_iUnion, inter_iInter]; rfl

Set Difference with Union Equals Intersection of Differences

Informal description

For any nonempty index type $\iota$, any set $s$ in a type $\beta$, and any family of sets $\{t_i\}_{i \in \iota}$ indexed by $\iota$, the set difference of $s$ with the union of all $t_i$ equals the intersection over all $i$ of the set difference $s \setminus t_i$. In symbols: $$ s \setminus \left(\bigcup_{i} t_i\right) = \bigcap_{i} (s \setminus t_i). $$

Set.diff_iInter theorem

(s : Set β) (t : ι → Set β) : (s \ ⋂ i, t i) = ⋃ i, s \ t i

Full source

theorem diff_iInter (s : Set β) (t : ι → Set β) : (s \ ⋂ i, t i) = ⋃ i, s \ t i := by
  rw [diff_eq, compl_iInter, inter_iUnion]; rfl

Set Difference of Intersection Equals Union of Differences

Informal description

For any set $s$ in a type $\beta$ and any family of sets $\{t_i\}_{i \in \iota}$ indexed by $\iota$ in $\beta$, the set difference of $s$ with the intersection of the $t_i$ equals the union of the set differences of $s$ with each $t_i$. In symbols: $$ s \setminus \left( \bigcap_{i} t_i \right) = \bigcup_{i} (s \setminus t_i). $$

Set.iUnion_inter_subset theorem

{ι α} {s t : ι → Set α} : ⋃ i, s i ∩ t i ⊆ (⋃ i, s i) ∩ ⋃ i, t i

Full source

theorem iUnion_inter_subset {ι α} {s t : ι → Set α} : ⋃ i, s i ∩ t i⋃ i, s i ∩ t i ⊆ (⋃ i, s i) ∩ ⋃ i, t i :=
  le_iSup_inf_iSup s t

Union of Pairwise Intersections is Subset of Intersection of Unions

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ and $\{t_i\}_{i \in \iota}$ in a type $\alpha$, the union of their pairwise intersections is a subset of the intersection of their unions, i.e., \[ \bigcup_{i} (s_i \cap t_i) \subseteq \left(\bigcup_{i} s_i\right) \cap \left(\bigcup_{i} t_i\right). \]

Set.iUnion_inter_of_monotone theorem

 {ι α} [Preorder ι] [IsDirected ι (· ≤ ·)] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) :
  ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i

Full source

theorem iUnion_inter_of_monotone {ι α} [Preorder ι] [IsDirected ι (· ≤ ·)] {s t : ι → Set α}
    (hs : Monotone s) (ht : Monotone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i :=
  iSup_inf_of_monotone hs ht

Union-Intersection Equality for Monotone Families of Sets

Informal description

Let $\iota$ be a preorder and $\alpha$ be a type. Suppose $\iota$ is directed with respect to the $\leq$ relation. For any two monotone families of sets $s, t : \iota \to \text{Set } \alpha$, the union of their intersections equals the intersection of their unions: \[ \bigcup_{i} (s_i \cap t_i) = \left(\bigcup_{i} s_i\right) \cap \left(\bigcup_{i} t_i\right). \]

Set.iUnion_inter_of_antitone theorem

 {ι α} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {s t : ι → Set α} (hs : Antitone s) (ht : Antitone t) :
  ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i

Full source

theorem iUnion_inter_of_antitone {ι α} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {s t : ι → Set α}
    (hs : Antitone s) (ht : Antitone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i :=
  iSup_inf_of_antitone hs ht

Union-Intersection Equality for Antitone Families of Sets

Informal description

Let $\iota$ be a preordered set directed with respect to the reverse order $\geq$, and let $\alpha$ be a type. For any two antitone families of sets $s, t : \iota \to \text{Set } \alpha$, the union of their pairwise intersections equals the intersection of their unions: \[ \bigcup_{i \in \iota} (s_i \cap t_i) = \left(\bigcup_{i \in \iota} s_i\right) \cap \left(\bigcup_{i \in \iota} t_i\right). \]

Set.iInter_union_of_monotone theorem

 {ι α} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) :
  ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i

Full source

theorem iInter_union_of_monotone {ι α} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {s t : ι → Set α}
    (hs : Monotone s) (ht : Monotone t) : ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i :=
  iInf_sup_of_monotone hs ht

Intersection-Union Equality for Monotone Families of Sets under Reverse Direction

Informal description

Let $\iota$ be a preordered set directed with respect to the reverse order $\geq$, and let $\alpha$ be a type. For any two monotone families of sets $s, t : \iota \to \text{Set } \alpha$, the intersection of their unions equals the union of their intersections: \[ \bigcap_{i \in \iota} (s_i \cup t_i) = \left(\bigcap_{i \in \iota} s_i\right) \cup \left(\bigcap_{i \in \iota} t_i\right). \]

Set.iInter_union_of_antitone theorem

 {ι α} [Preorder ι] [IsDirected ι (· ≤ ·)] {s t : ι → Set α} (hs : Antitone s) (ht : Antitone t) :
  ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i

Full source

theorem iInter_union_of_antitone {ι α} [Preorder ι] [IsDirected ι (· ≤ ·)] {s t : ι → Set α}
    (hs : Antitone s) (ht : Antitone t) : ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i :=
  iInf_sup_of_antitone hs ht

Intersection of Unions for Antitone Families of Sets

Informal description

Let $\iota$ be a preorder and suppose $\iota$ is directed with respect to the $\leq$ relation. For any two antitone families of sets $s, t : \iota \to \text{Set } \alpha$, the intersection of their unions satisfies: \[ \bigcap_i (s_i \cup t_i) = \left(\bigcap_i s_i\right) \cup \left(\bigcap_i t_i\right) \]

Set.iUnion_iInter_subset theorem

{s : ι → ι' → Set α} : (⋃ j, ⋂ i, s i j) ⊆ ⋂ i, ⋃ j, s i j

Full source

/-- An equality version of this lemma is `iUnion_iInter_of_monotone` in `Data.Set.Finite`. -/
theorem iUnion_iInter_subset {s : ι → ι' → Set α} : (⋃ j, ⋂ i, s i j) ⊆ ⋂ i, ⋃ j, s i j :=
  iSup_iInf_le_iInf_iSup (flip s)

Union of Intersections is Subset of Intersection of Unions

Informal description

For any family of sets $\{s_{i,j}\}_{i \in \iota, j \in \iota'}$ indexed by types $\iota$ and $\iota'$, the union over $j$ of the intersections over $i$ of $s_{i,j}$ is a subset of the intersection over $i$ of the unions over $j$ of $s_{i,j}$. In symbols: \[ \bigcup_{j} \bigcap_{i} s_{i,j} \subseteq \bigcap_{i} \bigcup_{j} s_{i,j} \]

Set.iUnion_option theorem

{ι} (s : Option ι → Set α) : ⋃ o, s o = s none ∪ ⋃ i, s (some i)

Full source

theorem iUnion_option {ι} (s : Option ι → Set α) : ⋃ o, s o = s none ∪ ⋃ i, s (some i) :=
  iSup_option s

Union Decomposition for Option-Indexed Family of Sets

Informal description

For any family of sets $s$ indexed by the type `Option ι`, the union of all sets in the family is equal to the union of the set corresponding to `none` and the union of all sets corresponding to `some i` for $i \in \iota$. In symbols: \[ \bigcup_{o \in \text{Option } \iota} s(o) = s(\text{none}) \cup \bigcup_{i \in \iota} s(\text{some } i). \]

Set.iInter_option theorem

{ι} (s : Option ι → Set α) : ⋂ o, s o = s none ∩ ⋂ i, s (some i)

Full source

theorem iInter_option {ι} (s : Option ι → Set α) : ⋂ o, s o = s none ∩ ⋂ i, s (some i) :=
  iInf_option s

Intersection of Option-Indexed Family of Sets

Informal description

For any family of sets $\{s_o\}_{o \in \text{Option } \iota}$ indexed by the type $\text{Option } \iota$, the intersection of all sets in the family is equal to the intersection of the set indexed by `none` with the intersection of all sets indexed by `some i` for $i \in \iota$. That is, \[ \bigcap_{o \in \text{Option } \iota} s_o = s_{\text{none}} \cap \bigcap_{i \in \iota} s_{\text{some } i}. \]

Set.iUnion_dite theorem

 (f : ∀ i, p i → Set α) (g : ∀ i, ¬p i → Set α) :
  ⋃ i, (if h : p i then f i h else g i h) = (⋃ (i) (h : p i), f i h) ∪ ⋃ (i) (h : ¬p i), g i h

Full source

theorem iUnion_dite (f : ∀ i, p i → Set α) (g : ∀ i, ¬p i → Set α) :
    ⋃ i, (if h : p i then f i h else g i h) = (⋃ (i) (h : p i), f i h) ∪ ⋃ (i) (h : ¬p i), g i h :=
  iSup_dite _ _ _

Union of Conditional Sets Equals Union of Cases

Informal description

Let $p$ be a predicate on an index set $I$, and let $f$ and $g$ be families of sets in $\alpha$ indexed by $I$ such that for each $i \in I$, $f_i$ is defined when $p(i)$ holds and $g_i$ is defined when $\neg p(i)$ holds. Then the union of all sets defined by the conditional expression (if $p(i)$ then $f_i$ else $g_i$) is equal to the union of all $f_i$ for which $p(i)$ holds, combined with the union of all $g_i$ for which $\neg p(i)$ holds. In symbols: \[ \bigcup_{i \in I} \left( \text{if } p(i) \text{ then } f_i \text{ else } g_i \right) = \left( \bigcup_{\substack{i \in I \\ p(i)}} f_i \right) \cup \left( \bigcup_{\substack{i \in I \\ \neg p(i)}} g_i \right) \]

Set.iUnion_ite theorem

(f g : ι → Set α) : ⋃ i, (if p i then f i else g i) = (⋃ (i) (_ : p i), f i) ∪ ⋃ (i) (_ : ¬p i), g i

Full source

theorem iUnion_ite (f g : ι → Set α) :
    ⋃ i, (if p i then f i else g i) = (⋃ (i) (_ : p i), f i) ∪ ⋃ (i) (_ : ¬p i), g i :=
  iUnion_dite _ _ _

Union of Conditional Sets Equals Union of Cases

Informal description

Let $p$ be a predicate on an index set $I$, and let $f$ and $g$ be families of sets in $\alpha$ indexed by $I$. Then the union of all sets defined by the conditional expression (if $p(i)$ then $f_i$ else $g_i$) is equal to the union of all $f_i$ for which $p(i)$ holds, combined with the union of all $g_i$ for which $\neg p(i)$ holds. In symbols: \[ \bigcup_{i \in I} \left( \text{if } p(i) \text{ then } f_i \text{ else } g_i \right) = \left( \bigcup_{\substack{i \in I \\ p(i)}} f_i \right) \cup \left( \bigcup_{\substack{i \in I \\ \neg p(i)}} g_i \right) \]

Set.iInter_dite theorem

 (f : ∀ i, p i → Set α) (g : ∀ i, ¬p i → Set α) :
  ⋂ i, (if h : p i then f i h else g i h) = (⋂ (i) (h : p i), f i h) ∩ ⋂ (i) (h : ¬p i), g i h

Full source

theorem iInter_dite (f : ∀ i, p i → Set α) (g : ∀ i, ¬p i → Set α) :
    ⋂ i, (if h : p i then f i h else g i h) = (⋂ (i) (h : p i), f i h) ∩ ⋂ (i) (h : ¬p i), g i h :=
  iInf_dite _ _ _

Intersection of Conditional Sets Equals Intersection of Cases

Informal description

For any indexed family of sets $\{f_i\}_{i \in I}$ where $f_i$ is defined when $p(i)$ holds, and $\{g_i\}_{i \in I}$ where $g_i$ is defined when $\neg p(i)$ holds, the intersection of the conditional sets equals the intersection of the $f_i$ sets for which $p(i)$ holds intersected with the intersection of the $g_i$ sets for which $\neg p(i)$ holds. That is, \[ \bigcap_{i \in I} \left( \text{if } p(i) \text{ then } f_i \text{ else } g_i \right) = \left( \bigcap_{\substack{i \in I \\ p(i)}} f_i \right) \cap \left( \bigcap_{\substack{i \in I \\ \neg p(i)}} g_i \right). \]

Set.iInter_ite theorem

(f g : ι → Set α) : ⋂ i, (if p i then f i else g i) = (⋂ (i) (_ : p i), f i) ∩ ⋂ (i) (_ : ¬p i), g i

Full source

theorem iInter_ite (f g : ι → Set α) :
    ⋂ i, (if p i then f i else g i) = (⋂ (i) (_ : p i), f i) ∩ ⋂ (i) (_ : ¬p i), g i :=
  iInter_dite _ _ _

Intersection of Conditional Sets via Predicate

Informal description

For any indexed family of sets $\{f_i\}_{i \in I}$ and $\{g_i\}_{i \in I}$, and any predicate $p$ on $I$, the intersection of the conditional sets equals the intersection of the $f_i$ sets for which $p(i)$ holds intersected with the intersection of the $g_i$ sets for which $\neg p(i)$ holds. That is, \[ \bigcap_{i \in I} \left( \text{if } p(i) \text{ then } f_i \text{ else } g_i \right) = \left( \bigcap_{\substack{i \in I \\ p(i)}} f_i \right) \cap \left( \bigcap_{\substack{i \in I \\ \neg p(i)}} g_i \right). \]

Set.iInter_false theorem

{s : False → Set α} : iInter s = univ

Full source

theorem iInter_false {s : False → Set α} : iInter s = univ :=
  iInf_false

Intersection over Empty Index Set is Universal Set

Informal description

For any family of sets $s$ indexed by the empty type `False`, the intersection of all sets in this family equals the universal set, i.e., $\bigcap_{i \in \text{False}} s(i) = \text{univ}$.

Set.iUnion_false theorem

{s : False → Set α} : iUnion s = ∅

Full source

theorem iUnion_false {s : False → Set α} : iUnion s = ∅ :=
  iSup_false

Union over False Indexed Family of Sets is Empty

Informal description

For any family of sets $s$ indexed by the type `False`, the union of all sets in the family is equal to the empty set. In other words, $\bigcup_{x : \text{False}} s(x) = \emptyset$.

Set.iInter_true theorem

{s : True → Set α} : iInter s = s trivial

Full source

@[simp]
theorem iInter_true {s : True → Set α} : iInter s = s trivial :=
  iInf_true

Intersection over True Indexed Family of Sets Equals Value at Trivial

Informal description

For any family of sets $s$ indexed by the type `True`, the intersection of all sets in the family is equal to $s(\text{trivial})$, where $\text{trivial}$ is the canonical element of `True`. In other words, $\bigcap_{x : \text{True}} s(x) = s(\text{trivial})$.

Set.iUnion_true theorem

{s : True → Set α} : iUnion s = s trivial

Full source

@[simp]
theorem iUnion_true {s : True → Set α} : iUnion s = s trivial :=
  iSup_true

Union over True Indexed Family of Sets

Informal description

For any family of sets $s$ indexed by the type `True`, the union of all sets in the family is equal to $s(\text{trivial})$, where $\text{trivial}$ is the canonical element of `True$. In other words, $\bigcup_{x : \text{True}} s(x) = s(\text{trivial})$.

Set.iInter_exists theorem

{p : ι → Prop} {f : Exists p → Set α} : ⋂ x, f x = ⋂ (i) (h : p i), f ⟨i, h⟩

Full source

@[simp]
theorem iInter_exists {p : ι → Prop} {f : Exists p → Set α} :
    ⋂ x, f x = ⋂ (i) (h : p i), f ⟨i, h⟩ :=
  iInf_exists

Intersection over Existence Indexed Family of Sets Equals Double Intersection

Informal description

For any predicate $p$ on a type $\iota$ and any family of sets $f$ indexed by the existence type $\exists i, p(i)$, the intersection of all sets in the family $f$ is equal to the double intersection over all $i \in \iota$ and all proofs $h$ that $p(i)$ holds, of the set $f(\langle i, h \rangle)$. In other words, \[ \bigcap_{x \in \exists i, p(i)} f(x) = \bigcap_{i \in \iota} \bigcap_{h : p(i)} f(\langle i, h \rangle). \]

Set.iUnion_exists theorem

{p : ι → Prop} {f : Exists p → Set α} : ⋃ x, f x = ⋃ (i) (h : p i), f ⟨i, h⟩

Full source

@[simp]
theorem iUnion_exists {p : ι → Prop} {f : Exists p → Set α} :
    ⋃ x, f x = ⋃ (i) (h : p i), f ⟨i, h⟩ :=
  iSup_exists

Union over Existence Indexed Family of Sets Equals Double Union

Informal description

For any predicate $p$ on a type $\iota$ and any family of sets $f$ indexed by the existence type $\{x \mid \exists i, p(i)\}$, the union of all sets in the family $f$ is equal to the double union over all $i \in \iota$ and all proofs $h$ that $p(i)$ holds, of the set $f(\langle i, h \rangle)$. In other words, \[ \bigcup_{x \in \exists i, p(i)} f(x) = \bigcup_{i \in \iota} \bigcup_{h : p(i)} f(\langle i, h \rangle). \]

Set.iUnion_empty theorem

: (⋃ _ : ι, ∅ : Set α) = ∅

Full source

@[simp]
theorem iUnion_empty : (⋃ _ : ι, ∅ : Set α) = ∅ :=
  iSup_bot

Union of Empty Sets is Empty

Informal description

The union of an empty set over any index type $\iota$ is the empty set, i.e., \[ \bigcup_{i \in \iota} \emptyset = \emptyset. \]

Set.iInter_univ theorem

: (⋂ _ : ι, univ : Set α) = univ

Full source

@[simp]
theorem iInter_univ : (⋂ _ : ι, univ : Set α) = univ :=
  iInf_top

Intersection of Universal Sets is Universal

Informal description

The intersection over an arbitrary index type $\iota$ of the universal set $\text{univ} : \text{Set} \alpha$ is equal to the universal set itself, i.e., $\bigcap_{i \in \iota} \text{univ} = \text{univ}$.

Set.iUnion_eq_empty theorem

: ⋃ i, s i = ∅ ↔ ∀ i, s i = ∅

Full source

@[simp]
theorem iUnion_eq_empty : ⋃ i, s i⋃ i, s i = ∅ ↔ ∀ i, s i = ∅ :=
  iSup_eq_bot

Union of Sets is Empty if and only if All Sets are Empty

Informal description

The union of a family of sets $\{s_i\}_{i \in \iota}$ is empty if and only if each set $s_i$ is empty. In other words: \[ \bigcup_{i \in \iota} s_i = \emptyset \leftrightarrow \forall i, s_i = \emptyset \]

Set.iInter_eq_univ theorem

: ⋂ i, s i = univ ↔ ∀ i, s i = univ

Full source

@[simp]
theorem iInter_eq_univ : ⋂ i, s i⋂ i, s i = univ ↔ ∀ i, s i = univ :=
  iInf_eq_top

Intersection Equals Universal Set if and only if All Sets Are Universal

Informal description

The intersection of a family of sets $\{s_i\}_{i \in I}$ over all indices $i$ equals the universal set if and only if each set $s_i$ in the family equals the universal set. In symbols: $$\bigcap_{i} s_i = \text{univ} \leftrightarrow \forall i, s_i = \text{univ}$$

Set.nonempty_iUnion theorem

: (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty

Full source

@[simp]
theorem nonempty_iUnion : (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty := by
  simp [nonempty_iff_ne_empty]

Nonemptiness of Union of Indexed Family of Sets

Informal description

The union $\bigcup_i s_i$ of a family of sets $\{s_i\}_{i\in I}$ is nonempty if and only if there exists an index $i$ such that $s_i$ is nonempty.

Set.nonempty_biUnion theorem

{t : Set α} {s : α → Set β} : (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty

Full source

theorem nonempty_biUnion {t : Set α} {s : α → Set β} :
    (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty := by simp

Nonemptiness of Bounded Union

Informal description

For any set $t \subseteq \alpha$ and any family of sets $s : \alpha \to \Set \beta$, the union $\bigcup_{i \in t} s_i$ is nonempty if and only if there exists an element $i \in t$ such that $s_i$ is nonempty.

Set.iUnion_nonempty_index theorem

(s : Set α) (t : s.Nonempty → Set β) : ⋃ h, t h = ⋃ x ∈ s, t ⟨x, ‹_›⟩

Full source

theorem iUnion_nonempty_index (s : Set α) (t : s.Nonempty → Set β) :
    ⋃ h, t h = ⋃ x ∈ s, t ⟨x, ‹_›⟩ :=
  iSup_exists

Union over Nonempty Index Set Equals Union over Elements

Informal description

For any nonempty set $s \subseteq \alpha$ and any family of sets $t$ indexed by the proof that $s$ is nonempty, the union of all $t(h)$ over all proofs $h$ of nonemptiness equals the union of $t(\langle x, \_ \rangle)$ over all $x \in s$.

Set.iInter_iInter_eq_left theorem

{b : β} {s : ∀ x : β, x = b → Set α} : ⋂ (x) (h : x = b), s x h = s b rfl

Full source

@[simp]
theorem iInter_iInter_eq_left {b : β} {s : ∀ x : β, x = b → Set α} :
    ⋂ (x) (h : x = b), s x h = s b rfl :=
  iInf_iInf_eq_left

Nested Intersection Equality for Left-Equal Index

Informal description

For any element $b$ of type $\beta$ and any family of sets $s$ indexed by elements $x$ of $\beta$ and proofs that $x = b$, the intersection $\bigcap_{x} \bigcap_{h : x = b} s(x, h)$ is equal to $s(b, \text{rfl})$, where $\text{rfl}$ is the reflexivity proof that $b = b$.

Set.iInter_iInter_eq_right theorem

{b : β} {s : ∀ x : β, b = x → Set α} : ⋂ (x) (h : b = x), s x h = s b rfl

Full source

@[simp]
theorem iInter_iInter_eq_right {b : β} {s : ∀ x : β, b = x → Set α} :
    ⋂ (x) (h : b = x), s x h = s b rfl :=
  iInf_iInf_eq_right

Nested Intersection Equality for Right-Equal Index

Informal description

For any element $b$ of type $\beta$ and any family of sets $s$ indexed by elements $x$ of $\beta$ with the condition $b = x$, the intersection $\bigcap_{x} \bigcap_{h : b = x} s(x, h)$ is equal to $s(b, \text{rfl})$, where $\text{rfl}$ is the reflexivity proof of $b = b$.

Set.iUnion_iUnion_eq_left theorem

{b : β} {s : ∀ x : β, x = b → Set α} : ⋃ (x) (h : x = b), s x h = s b rfl

Full source

@[simp]
theorem iUnion_iUnion_eq_left {b : β} {s : ∀ x : β, x = b → Set α} :
    ⋃ (x) (h : x = b), s x h = s b rfl :=
  iSup_iSup_eq_left

Union of Sets Indexed by Equality to Fixed Point Equals Value at Reflexivity

Informal description

For any type $\beta$, element $b \in \beta$, and family of sets $s$ indexed by pairs $(x, h)$ where $x \in \beta$ and $h$ is a proof that $x = b$, the union of all sets $s(x, h)$ over such pairs equals $s(b, \text{rfl})$, where $\text{rfl}$ is the reflexivity proof that $b = b$. In symbols: $$ \bigcup_{x \in \beta} \bigcup_{h : x = b} s(x, h) = s(b, \text{rfl}) $$

Set.iUnion_iUnion_eq_right theorem

{b : β} {s : ∀ x : β, b = x → Set α} : ⋃ (x) (h : b = x), s x h = s b rfl

Full source

@[simp]
theorem iUnion_iUnion_eq_right {b : β} {s : ∀ x : β, b = x → Set α} :
    ⋃ (x) (h : b = x), s x h = s b rfl :=
  iSup_iSup_eq_right

Union Reduction for Indexed Family with Equality Constraint

Informal description

For any type $\beta$, element $b \in \beta$, and family of sets $s$ indexed by pairs $(x, h)$ where $h$ is a proof that $b = x$, the union of all $s(x,h)$ equals $s(b,\text{rfl})$, where $\text{rfl}$ is the reflexivity proof that $b = b$. In symbols: $$ \bigcup_{x} \bigcup_{h : b = x} s(x,h) = s(b, \text{rfl}) $$

Set.iInter_or theorem

{p q : Prop} (s : p ∨ q → Set α) : ⋂ h, s h = (⋂ h : p, s (Or.inl h)) ∩ ⋂ h : q, s (Or.inr h)

Full source

theorem iInter_or {p q : Prop} (s : p ∨ q → Set α) :
    ⋂ h, s h = (⋂ h : p, s (Or.inl h)) ∩ ⋂ h : q, s (Or.inr h) :=
  iInf_or

Intersection over Disjunction Equals Intersection of Intersections

Informal description

For any two propositions $p$ and $q$, and for any family of sets $s$ indexed by $p ∨ q$ (i.e., $s$ takes a proof of either $p$ or $q$ and returns a set in $\alpha$), the intersection of all sets in this family equals the intersection of the sets corresponding to $p$ intersected with the intersection of the sets corresponding to $q$. In symbols: \[ \bigcap_{h:p∨q} s(h) = \left(\bigcap_{h:p} s(\text{Or.inl }h)\right) ∩ \left(\bigcap_{h:q} s(\text{Or.inr }h)\right) \]

Set.iUnion_or theorem

{p q : Prop} (s : p ∨ q → Set α) : ⋃ h, s h = (⋃ i, s (Or.inl i)) ∪ ⋃ j, s (Or.inr j)

Full source

theorem iUnion_or {p q : Prop} (s : p ∨ q → Set α) :
    ⋃ h, s h = (⋃ i, s (Or.inl i)) ∪ ⋃ j, s (Or.inr j) :=
  iSup_or

Union over Disjunction Equals Union of Unions

Informal description

For any two propositions $p$ and $q$, and any family of sets $s$ indexed by $p \lor q$, the union of all sets $s(h)$ over all proofs $h$ of $p \lor q$ is equal to the union of the sets indexed by $p$ (via $\text{Or.inl}$) and the sets indexed by $q$ (via $\text{Or.inr}$). That is, \[ \bigcup_{h : p \lor q} s(h) = \left(\bigcup_{i : p} s(\text{Or.inl }i)\right) \cup \left(\bigcup_{j : q} s(\text{Or.inr }j)\right). \]

Set.iUnion_and theorem

{p q : Prop} (s : p ∧ q → Set α) : ⋃ h, s h = ⋃ (hp) (hq), s ⟨hp, hq⟩

Full source

theorem iUnion_and {p q : Prop} (s : p ∧ q → Set α) : ⋃ h, s h = ⋃ (hp) (hq), s ⟨hp, hq⟩ :=
  iSup_and

Union over Conjunction Equals Double Union

Informal description

For any two propositions $p$ and $q$ and any family of sets $s$ indexed by $p ∧ q$ in a type $\alpha$, the union over all proofs $h$ of $p ∧ q$ of $s(h)$ is equal to the union over all proofs $hp$ of $p$ and all proofs $hq$ of $q$ of $s(\langle hp, hq \rangle)$. In symbols: $$ \bigcup_{h : p ∧ q} s(h) = \bigcup_{hp : p} \bigcup_{hq : q} s(\langle hp, hq \rangle) $$

Set.iInter_and theorem

{p q : Prop} (s : p ∧ q → Set α) : ⋂ h, s h = ⋂ (hp) (hq), s ⟨hp, hq⟩

Full source

theorem iInter_and {p q : Prop} (s : p ∧ q → Set α) : ⋂ h, s h = ⋂ (hp) (hq), s ⟨hp, hq⟩ :=
  iInf_and

Intersection over Conjunction of Propositions Equals Nested Intersection

Informal description

For any two propositions $p$ and $q$ and any family of sets $s$ indexed by $p \land q$, the intersection of all sets $s(h)$ where $h$ is a proof of $p \land q$ is equal to the intersection over all proofs $hp$ of $p$ and $hq$ of $q$ of the sets $s(\langle hp, hq \rangle)$. In other words: \[ \bigcap_{h : p \land q} s(h) = \bigcap_{hp : p} \bigcap_{hq : q} s(\langle hp, hq \rangle) \]

Set.iUnion_comm theorem

(s : ι → ι' → Set α) : ⋃ (i) (i'), s i i' = ⋃ (i') (i), s i i'

Full source

theorem iUnion_comm (s : ι → ι' → Set α) : ⋃ (i) (i'), s i i' = ⋃ (i') (i), s i i' :=
  iSup_comm

Commutativity of Double Union

Informal description

For any family of sets $\{s_{i,i'}\}_{i \in \iota, i' \in \iota'}$ indexed by two types $\iota$ and $\iota'$, the union over $i$ and then $i'$ is equal to the union over $i'$ and then $i$. That is, \[ \bigcup_{i \in \iota} \bigcup_{i' \in \iota'} s_{i,i'} = \bigcup_{i' \in \iota'} \bigcup_{i \in \iota} s_{i,i'}. \]

Set.iInter_comm theorem

(s : ι → ι' → Set α) : ⋂ (i) (i'), s i i' = ⋂ (i') (i), s i i'

Full source

theorem iInter_comm (s : ι → ι' → Set α) : ⋂ (i) (i'), s i i' = ⋂ (i') (i), s i i' :=
  iInf_comm

Commutativity of Double Intersection

Informal description

For any family of sets $s : \iota \to \iota' \to \text{Set} \alpha$, the intersection over all pairs $(i, i')$ is equal to the intersection over all pairs $(i', i)$. That is, \[ \bigcap_{i} \bigcap_{i'} s(i, i') = \bigcap_{i'} \bigcap_{i} s(i, i'). \]

Set.iUnion_sigma theorem

{γ : α → Type*} (s : Sigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩

Full source

theorem iUnion_sigma {γ : α → Type*} (s : Sigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩ :=
  iSup_sigma

Double Union Decomposition for Sigma Type

Informal description

Let $γ$ be a type family indexed by $α$, and let $s$ be a function that assigns a subset of $β$ to each pair $(i,a)$ where $i ∈ α$ and $a ∈ γ(i)$. Then the union of all sets $s(i,a)$ over all pairs $(i,a)$ equals the union over all $i ∈ α$ of the union over all $a ∈ γ(i)$ of $s(i,a)$. In symbols: \[ \bigcup_{(i,a) ∈ Σ_{i∈α} γ(i)} s(i,a) = \bigcup_{i∈α} \bigcup_{a∈γ(i)} s(i,a) \]

Set.iUnion_sigma' theorem

{γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋃ i, ⋃ a, s i a = ⋃ ia : Sigma γ, s ia.1 ia.2

Full source

theorem iUnion_sigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) :
    ⋃ i, ⋃ a, s i a = ⋃ ia : Sigma γ, s ia.1 ia.2 :=
  iSup_sigma' _

Double Union Equivalence for Dependent Indexed Family of Sets

Informal description

For any family of sets $\{s_i(a)\}_{i \in \alpha, a \in \gamma_i}$ indexed by a dependent type $\Sigma \gamma$ (where $\gamma : \alpha \to \text{Type}$), the union over all pairs $(i,a)$ is equal to the double union over $i$ and then over $a$: \[ \bigcup_{i \in \alpha} \bigcup_{a \in \gamma_i} s_i(a) = \bigcup_{(i,a) \in \Sigma \gamma} s_i(a) \]

Set.iInter_sigma theorem

{γ : α → Type*} (s : Sigma γ → Set β) : ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩

Full source

theorem iInter_sigma {γ : α → Type*} (s : Sigma γ → Set β) : ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩ :=
  iInf_sigma

Nested Intersection Equality for Dependent Sums of Sets

Informal description

For any family of types $\gamma : \alpha \to \text{Type}^*$ and any function $s : \Sigma \gamma \to \text{Set} \beta$, the intersection of all sets $s(ia)$ over all pairs $ia = \langle i, a \rangle$ in the dependent sum $\Sigma \gamma$ is equal to the intersection over all indices $i \in \alpha$ of the intersection over all $a \in \gamma i$ of the sets $s(\langle i, a \rangle)$. In symbols: \[ \bigcap_{ia \in \Sigma \gamma} s(ia) = \bigcap_{i \in \alpha} \bigcap_{a \in \gamma i} s(\langle i, a \rangle). \]

Set.iInter_sigma' theorem

{γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋂ i, ⋂ a, s i a = ⋂ ia : Sigma γ, s ia.1 ia.2

Full source

theorem iInter_sigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) :
    ⋂ i, ⋂ a, s i a = ⋂ ia : Sigma γ, s ia.1 ia.2 :=
  iInf_sigma' _

Double Intersection Equals Sigma-Type Intersection for Indexed Family of Sets

Informal description

Let $α$ be a type, $β$ be another type, and for each $i \in α$, let $γ_i$ be a type. Given a family of sets $s_i(a) \subseteq β$ indexed by $i \in α$ and $a \in γ_i$, the intersection over all $i$ and $a$ of $s_i(a)$ is equal to the intersection over all pairs $(i,a)$ in the dependent sum type $\Sigma i, γ_i$ of $s_i(a)$. In symbols: \[ \bigcap_{i \in α} \bigcap_{a \in γ_i} s_i(a) = \bigcap_{(i,a) \in \Sigma i, γ_i} s_i(a) \]

Set.iUnion₂_comm theorem

 (s : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Set α) : ⋃ (i₁) (j₁) (i₂) (j₂), s i₁ j₁ i₂ j₂ = ⋃ (i₂) (j₂) (i₁) (j₁), s i₁ j₁ i₂ j₂

Full source

theorem iUnion₂_comm (s : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Set α) :
    ⋃ (i₁) (j₁) (i₂) (j₂), s i₁ j₁ i₂ j₂ = ⋃ (i₂) (j₂) (i₁) (j₁), s i₁ j₁ i₂ j₂ :=
  iSup₂_comm _

Commutation of Double Indexed Union

Informal description

For any family of sets $s_{i_1,j_1,i_2,j_2}$ indexed by $i_1 \in \kappa_1$, $j_1 \in \kappa_1(i_1)$, $i_2 \in \kappa_2$, and $j_2 \in \kappa_2(i_2)$, the union over all indices commutes as follows: \[ \bigcup_{i_1} \bigcup_{j_1} \bigcup_{i_2} \bigcup_{j_2} s_{i_1,j_1,i_2,j_2} = \bigcup_{i_2} \bigcup_{j_2} \bigcup_{i_1} \bigcup_{j_1} s_{i_1,j_1,i_2,j_2} \]

Set.iInter₂_comm theorem

 (s : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Set α) : ⋂ (i₁) (j₁) (i₂) (j₂), s i₁ j₁ i₂ j₂ = ⋂ (i₂) (j₂) (i₁) (j₁), s i₁ j₁ i₂ j₂

Full source

theorem iInter₂_comm (s : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Set α) :
    ⋂ (i₁) (j₁) (i₂) (j₂), s i₁ j₁ i₂ j₂ = ⋂ (i₂) (j₂) (i₁) (j₁), s i₁ j₁ i₂ j₂ :=
  iInf₂_comm _

Commutation of Double Indexed Intersection

Informal description

For any family of sets $s_{i_1,j_1,i_2,j_2}$ indexed by $i_1 \in \kappa_1$, $j_1 \in \kappa_1(i_1)$, $i_2 \in \kappa_2$, and $j_2 \in \kappa_2(i_2)$, the intersection over all indices commutes as follows: \[ \bigcap_{i_1} \bigcap_{j_1} \bigcap_{i_2} \bigcap_{j_2} s_{i_1,j_1,i_2,j_2} = \bigcap_{i_2} \bigcap_{j_2} \bigcap_{i_1} \bigcap_{j_1} s_{i_1,j_1,i_2,j_2} \]

Set.biUnion_and theorem

 (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
  ⋃ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h = ⋃ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩

Full source

@[simp]
theorem biUnion_and (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
    ⋃ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h =
      ⋃ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩ := by
  simp only [iUnion_and, @iUnion_comm _ ι']

Union over Conjunction Equals Nested Union

Informal description

For any family of sets $\{s_{x,y}\}_{x \in \iota, y \in \iota'}$ in a type $\alpha$, indexed by pairs $(x,y)$ where $x$ satisfies a predicate $p$ and $y$ satisfies a predicate $q_x$, the union over all $x \in \iota$, $y \in \iota'$ with $p(x) \land q_x(y)$ of $s_{x,y}$ is equal to the union over all $x \in \iota$ with $p(x)$, and all $y \in \iota'$ with $q_x(y)$, of $s_{x,y}$. In symbols: \[ \bigcup_{\substack{x \in \iota \\ y \in \iota' \\ p(x) \land q_x(y)}} s_{x,y} = \bigcup_{\substack{x \in \iota \\ p(x)}} \bigcup_{\substack{y \in \iota' \\ q_x(y)}} s_{x,y} \]

Set.biUnion_and' theorem

 (p : ι' → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p y ∧ q x y → Set α) :
  ⋃ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h = ⋃ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y ⟨hy, hx⟩

Full source

@[simp]
theorem biUnion_and' (p : ι' → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p y ∧ q x y → Set α) :
    ⋃ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h =
      ⋃ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y ⟨hy, hx⟩ := by
  simp only [iUnion_and, @iUnion_comm _ ι]

Bounded Union over Conjunction Equals Reordered Union

Informal description

For any family of sets $\{s_{x,y}\}_{x \in \iota, y \in \iota'}$ indexed by types $\iota$ and $\iota'$, where each set $s_{x,y}$ is defined for pairs $(x,y)$ satisfying $p(y) \land q(x,y)$, the following equality holds: \[ \bigcup_{x \in \iota} \bigcup_{y \in \iota'} \bigcup_{h : p(y) \land q(x,y)} s_{x,y}(h) = \bigcup_{y \in \iota'} \bigcup_{h_y : p(y)} \bigcup_{x \in \iota} \bigcup_{h_x : q(x,y)} s_{x,y}(\langle h_y, h_x \rangle) \]

Set.biInter_and theorem

 (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
  ⋂ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h = ⋂ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩

Full source

@[simp]
theorem biInter_and (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
    ⋂ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h =
      ⋂ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩ := by
  simp only [iInter_and, @iInter_comm _ ι']

Nested Bounded Intersection over Conjunctive Conditions

Informal description

For any family of sets $s$ indexed by pairs $(x, y)$ where $x$ satisfies $p(x)$ and $y$ satisfies $q(x, y)$, the intersection over all such pairs equals the nested intersection over all $x$ satisfying $p(x)$ and then all $y$ satisfying $q(x, y)$. That is, \[ \bigcap_{x \in \iota} \bigcap_{y \in \iota'} \bigcap_{h : p(x) \land q(x, y)} s(x, y, h) = \bigcap_{x \in \iota} \bigcap_{h_x : p(x)} \bigcap_{y \in \iota'} \bigcap_{h_y : q(x, y)} s(x, y, \langle h_x, h_y \rangle). \]

Set.biInter_and' theorem

 (p : ι' → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p y ∧ q x y → Set α) :
  ⋂ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h = ⋂ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y ⟨hy, hx⟩

Full source

@[simp]
theorem biInter_and' (p : ι' → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p y ∧ q x y → Set α) :
    ⋂ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h =
      ⋂ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y ⟨hy, hx⟩ := by
  simp only [iInter_and, @iInter_comm _ ι]

Nested Bounded Intersection over Conjunction of Conditions

Informal description

For any family of sets $s : \iota \to \iota' \to \text{Set} \alpha$ indexed by pairs $(x,y)$ where $p(y)$ and $q(x,y)$ hold, the intersection over all such triples $(x,y,h)$ with $h : p(y) \land q(x,y)$ is equal to the nested intersection over all $y$ with $p(y)$, then over all $x$ with $q(x,y)$. That is, \[ \bigcap_{x} \bigcap_{y} \bigcap_{h : p(y) \land q(x,y)} s(x,y,h) = \bigcap_{y} \bigcap_{hy : p(y)} \bigcap_{x} \bigcap_{hx : q(x,y)} s(x,y,\langle hy, hx \rangle). \]

Set.iUnion_iUnion_eq_or_left theorem

 {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
  ⋃ (x) (h), s x h = s b (Or.inl rfl) ∪ ⋃ (x) (h : p x), s x (Or.inr h)

Full source

@[simp]
theorem iUnion_iUnion_eq_or_left {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
    ⋃ (x) (h), s x h = s b (Or.inl rfl) ∪ ⋃ (x) (h : p x), s x (Or.inr h) := by
  simp only [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]

Union Decomposition over Disjunctive Indexing

Informal description

For any type $\beta$, element $b \in \beta$, predicate $p$ on $\beta$, and family of sets $\{s(x,h)\}$ indexed by pairs $(x,h)$ where $x \in \beta$ and $h$ is a proof that either $x = b$ or $p(x)$ holds, the union of all such sets equals the union of the set $s(b, \text{Or.inl}(\text{rfl}))$ (where $\text{rfl}$ is the reflexivity proof that $b = b$) with the union of all sets $s(x, \text{Or.inr}(h))$ where $h$ is a proof that $p(x)$ holds. In symbols: $$ \bigcup_{x \in \beta} \bigcup_{h : x = b \lor p(x)} s(x,h) = s(b, \text{Or.inl}(\text{rfl})) \cup \left( \bigcup_{x \in \beta} \bigcup_{h : p(x)} s(x, \text{Or.inr}(h)) \right) $$

Set.iInter_iInter_eq_or_left theorem

 {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
  ⋂ (x) (h), s x h = s b (Or.inl rfl) ∩ ⋂ (x) (h : p x), s x (Or.inr h)

Full source

@[simp]
theorem iInter_iInter_eq_or_left {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
    ⋂ (x) (h), s x h = s b (Or.inl rfl) ∩ ⋂ (x) (h : p x), s x (Or.inr h) := by
  simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]

Nested Intersection Equality for Disjunctive Index with Left Option

Informal description

For any element $b$ of type $\beta$, any predicate $p$ on $\beta$, and any family of sets $s$ indexed by elements $x$ of $\beta$ and proofs that $x = b$ or $p(x)$, the intersection $\bigcap_{x} \bigcap_{h : x = b \lor p(x)} s(x, h)$ is equal to the intersection of $s(b, \text{Or.inl } \text{rfl})$ with $\bigcap_{x} \bigcap_{h : p(x)} s(x, \text{Or.inr } h)$.

Set.iUnion_sum theorem

{s : α ⊕ β → Set γ} : ⋃ x, s x = (⋃ x, s (.inl x)) ∪ ⋃ x, s (.inr x)

Full source

lemma iUnion_sum {s : α ⊕ β → Set γ} : ⋃ x, s x = (⋃ x, s (.inl x)) ∪ ⋃ x, s (.inr x) := iSup_sum

Union Decomposition over Disjoint Union Index

Informal description

For any family of sets $\{s_x\}_{x \in \alpha \oplus \beta}$ indexed by the disjoint union of types $\alpha$ and $\beta$, the union of all sets in the family equals the union of the sets indexed by $\alpha$ combined with the union of the sets indexed by $\beta$. That is, $$\bigcup_{x \in \alpha \oplus \beta} s_x = \left(\bigcup_{x \in \alpha} s_{\text{inl}(x)}\right) \cup \left(\bigcup_{x \in \beta} s_{\text{inr}(x)}\right)$$ where $\text{inl}$ and $\text{inr}$ are the canonical injections into the disjoint union.

Set.iInter_sum theorem

{s : α ⊕ β → Set γ} : ⋂ x, s x = (⋂ x, s (.inl x)) ∩ ⋂ x, s (.inr x)

Full source

lemma iInter_sum {s : α ⊕ β → Set γ} : ⋂ x, s x = (⋂ x, s (.inl x)) ∩ ⋂ x, s (.inr x) := iInf_sum

Intersection over Disjoint Union Equals Intersection of Components

Informal description

For any family of sets $s$ indexed by the disjoint union type $\alpha \oplus \beta$, the intersection of all sets in the family equals the intersection of the sets indexed by $\alpha$ intersected with the intersection of the sets indexed by $\beta$. That is, \[ \bigcap_{x \in \alpha \oplus \beta} s(x) = \left(\bigcap_{x \in \alpha} s(\mathrm{inl}(x))\right) \cap \left(\bigcap_{x \in \beta} s(\mathrm{inr}(x))\right). \]

Set.iUnion_psigma theorem

{γ : α → Type*} (s : PSigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩

Full source

theorem iUnion_psigma {γ : α → Type*} (s : PSigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩ :=
  iSup_psigma _

Union over Dependent Pairs Equals Nested Unions

Informal description

For any family of sets $\{s_{i,a}\}_{i \in \alpha, a \in \gamma_i}$ indexed by a dependent pair $(i,a) \in \Sigma_{i \in \alpha} \gamma_i$, the union of all sets $s_{i,a}$ is equal to the union over all indices $i \in \alpha$ of the union over all $a \in \gamma_i$ of the sets $s_{i,a}$. In symbols: \[ \bigcup_{(i,a) \in \Sigma_{i \in \alpha} \gamma_i} s_{i,a} = \bigcup_{i \in \alpha} \bigcup_{a \in \gamma_i} s_{i,a} \]

Set.iUnion_psigma' theorem

{γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋃ i, ⋃ a, s i a = ⋃ ia : PSigma γ, s ia.1 ia.2

Full source

/-- A reversed version of `iUnion_psigma` with a curried map. -/
theorem iUnion_psigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) :
    ⋃ i, ⋃ a, s i a = ⋃ ia : PSigma γ, s ia.1 ia.2 :=
  iSup_psigma' _

Union of Unions Equals Union over Dependent Pairs

Informal description

For any family of sets $\{s_i(a)\}_{i \in \alpha, a \in \gamma_i}$ indexed by a dependent type $\gamma : \alpha \to \text{Type}^*$, the union of all sets $s_i(a)$ over all indices $i \in \alpha$ and all parameters $a \in \gamma_i$ is equal to the union of all sets $s_{i}(a)$ indexed by the dependent pair type $\Sigma (i : \alpha), \gamma_i$. In symbols: \[ \bigcup_{i \in \alpha} \bigcup_{a \in \gamma_i} s_i(a) = \bigcup_{(i,a) \in \Sigma (i : \alpha), \gamma_i} s_i(a) \]

Set.iInter_psigma theorem

{γ : α → Type*} (s : PSigma γ → Set β) : ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩

Full source

theorem iInter_psigma {γ : α → Type*} (s : PSigma γ → Set β) : ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩ :=
  iInf_psigma _

Iterated Intersection over Sigma-Type Indexing

Informal description

For any family of types $\gamma : \alpha \to \text{Type*}$ and any collection of sets $s : \text{PSigma} \gamma \to \text{Set} \beta$, the intersection over all pairs $(i,a)$ in the sigma type $\text{PSigma} \gamma$ equals the iterated intersection over all indices $i$ and then over all elements $a$ of $\gamma i$. That is, \[ \bigcap_{(i,a) \in \Sigma \gamma} s(i,a) = \bigcap_{i} \bigcap_{a \in \gamma i} s(i,a). \]

Set.iInter_psigma' theorem

{γ : α → Type*} (s : ∀ i, γ i → Set β) : ⋂ i, ⋂ a, s i a = ⋂ ia : PSigma γ, s ia.1 ia.2

Full source

/-- A reversed version of `iInter_psigma` with a curried map. -/
theorem iInter_psigma' {γ : α → Type*} (s : ∀ i, γ i → Set β) :
    ⋂ i, ⋂ a, s i a = ⋂ ia : PSigma γ, s ia.1 ia.2 :=
  iInf_psigma' _

Double Intersection Equals Dependent Pair Intersection

Informal description

For any family of sets $\{s_i(a)\}_{i \in \alpha, a \in \gamma_i}$ indexed by a dependent type $\gamma : \alpha \to \text{Type*}$, the intersection over all $i \in \alpha$ and $a \in \gamma_i$ of $s_i(a)$ is equal to the intersection over all pairs $(i, a) \in \Sigma i, \gamma_i$ of $s_i(a)$. In symbols: \[ \bigcap_{i \in \alpha} \bigcap_{a \in \gamma_i} s_i(a) = \bigcap_{(i,a) \in \Sigma i, \gamma_i} s_i(a) \]

Set.mem_biUnion theorem

{s : Set α} {t : α → Set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) : y ∈ ⋃ x ∈ s, t x

Full source

/-- A specialization of `mem_iUnion₂`. -/
theorem mem_biUnion {s : Set α} {t : α → Set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) :
    y ∈ ⋃ x ∈ s, t x :=
  mem_iUnion₂_of_mem xs ytx

Element in Bounded Union if in Some Set of the Family

Informal description

For any set $s \subseteq \alpha$, any family of sets $\{t(x)\}_{x \in \alpha}$ in $\beta$, and any elements $x \in s$ and $y \in t(x)$, we have $y \in \bigcup_{x \in s} t(x)$.

Set.mem_biInter theorem

{s : Set α} {t : α → Set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) : y ∈ ⋂ x ∈ s, t x

Full source

/-- A specialization of `mem_iInter₂`. -/
theorem mem_biInter {s : Set α} {t : α → Set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) :
    y ∈ ⋂ x ∈ s, t x :=
  mem_iInter₂_of_mem h

Element in All Sets of Family Implies Element in Bounded Intersection

Informal description

For any set $s \subseteq \alpha$, any family of sets $\{t(x)\}_{x \in \alpha}$ in $\beta$, and any element $y \in \beta$, if $y$ belongs to $t(x)$ for every $x \in s$, then $y$ belongs to the bounded intersection $\bigcap_{x \in s} t(x)$.

Set.subset_biUnion_of_mem theorem

{s : Set α} {u : α → Set β} {x : α} (xs : x ∈ s) : u x ⊆ ⋃ x ∈ s, u x

Full source

/-- A specialization of `subset_iUnion₂`. -/
theorem subset_biUnion_of_mem {s : Set α} {u : α → Set β} {x : α} (xs : x ∈ s) :
    u x ⊆ ⋃ x ∈ s, u x :=
  subset_iUnion₂ (s := fun i _ => u i) x xs

Inclusion of Set in Bounded Union

Informal description

For any set $s$ in a type $\alpha$, any family of sets $u : \alpha \to \text{Set} \beta$, and any element $x \in s$, the set $u(x)$ is a subset of the bounded union $\bigcup_{x \in s} u(x)$.

Set.biInter_subset_of_mem theorem

{s : Set α} {t : α → Set β} {x : α} (xs : x ∈ s) : ⋂ x ∈ s, t x ⊆ t x

Full source

/-- A specialization of `iInter₂_subset`. -/
theorem biInter_subset_of_mem {s : Set α} {t : α → Set β} {x : α} (xs : x ∈ s) :
    ⋂ x ∈ s, t x⋂ x ∈ s, t x ⊆ t x :=
  iInter₂_subset x xs

Intersection of Indexed Family is Subset of Member Set

Informal description

For any set $s$ in a type $\alpha$, any family of sets $t : \alpha \to \text{Set} \beta$, and any element $x \in s$, the intersection $\bigcap_{x \in s} t(x)$ is a subset of $t(x)$.

Set.biInter_subset_biUnion theorem

{s : Set α} (hs : s.Nonempty) {t : α → Set β} : ⋂ x ∈ s, t x ⊆ ⋃ x ∈ s, t x

Full source

lemma biInter_subset_biUnion {s : Set α} (hs : s.Nonempty) {t : α → Set β} :
    ⋂ x ∈ s, t x⋂ x ∈ s, t x ⊆ ⋃ x ∈ s, t x := biInf_le_biSup hs

Intersection of Nonempty Family is Subset of Union

Informal description

For any nonempty set $s$ in a type $\alpha$ and any family of sets $t : \alpha \to \text{Set} \beta$, the intersection $\bigcap_{x \in s} t(x)$ is a subset of the union $\bigcup_{x \in s} t(x)$.

Set.biUnion_subset_biUnion_left theorem

{s s' : Set α} {t : α → Set β} (h : s ⊆ s') : ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x

Full source

theorem biUnion_subset_biUnion_left {s s' : Set α} {t : α → Set β} (h : s ⊆ s') :
    ⋃ x ∈ s, t x⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x :=
  iUnion₂_subset fun _ hx => subset_biUnion_of_mem <| h hx

Monotonicity of Bounded Union with Respect to Set Inclusion

Informal description

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

Set.biInter_subset_biInter_left theorem

{s s' : Set α} {t : α → Set β} (h : s' ⊆ s) : ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x

Full source

theorem biInter_subset_biInter_left {s s' : Set α} {t : α → Set β} (h : s' ⊆ s) :
    ⋂ x ∈ s, t x⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x :=
  subset_iInter₂ fun _ hx => biInter_subset_of_mem <| h hx

Monotonicity of Bounded Intersection with Respect to Superset Inclusion

Informal description

For any sets $s$ and $s'$ in a type $\alpha$ such that $s' \subseteq s$, and any family of sets $t : \alpha \to \text{Set} \beta$, the intersection $\bigcap_{x \in s} t(x)$ is a subset of the intersection $\bigcap_{x \in s'} t(x)$.

Set.biUnion_mono theorem

 {s s' : Set α} {t t' : α → Set β} (hs : s' ⊆ s) (h : ∀ x ∈ s, t x ⊆ t' x) : ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x

Full source

theorem biUnion_mono {s s' : Set α} {t t' : α → Set β} (hs : s' ⊆ s) (h : ∀ x ∈ s, t x ⊆ t' x) :
    ⋃ x ∈ s', t x⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x :=
  (biUnion_subset_biUnion_left hs).trans <| iUnion₂_mono h

Monotonicity of Bounded Union with Respect to Set Inclusion and Family Inclusion

Informal description

For any sets $s$ and $s'$ in a type $\alpha$ such that $s' \subseteq s$, and any families of sets $t, t' : \alpha \to \text{Set} \beta$ such that $t(x) \subseteq t'(x)$ for all $x \in s$, we have $$\bigcup_{x \in s'} t(x) \subseteq \bigcup_{x \in s} t'(x).$$

Set.biInter_mono theorem

 {s s' : Set α} {t t' : α → Set β} (hs : s ⊆ s') (h : ∀ x ∈ s, t x ⊆ t' x) : ⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x

Full source

theorem biInter_mono {s s' : Set α} {t t' : α → Set β} (hs : s ⊆ s') (h : ∀ x ∈ s, t x ⊆ t' x) :
    ⋂ x ∈ s', t x⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x :=
  (biInter_subset_biInter_left hs).trans <| iInter₂_mono h

Monotonicity of Bounded Intersection with Respect to Subset Inclusion and Family Inclusion

Informal description

For any sets $s$ and $s'$ in a type $\alpha$ such that $s \subseteq s'$, and any families of sets $t, t' : \alpha \to \text{Set} \beta$ such that $t(x) \subseteq t'(x)$ for all $x \in s$, we have $$\bigcap_{x \in s'} t(x) \subseteq \bigcap_{x \in s} t'(x).$$

Set.biUnion_eq_iUnion theorem

(s : Set α) (t : ∀ x ∈ s, Set β) : ⋃ x ∈ s, t x ‹_› = ⋃ x : s, t x x.2

Full source

theorem biUnion_eq_iUnion (s : Set α) (t : ∀ x ∈ s, Set β) :
    ⋃ x ∈ s, t x ‹_› = ⋃ x : s, t x x.2 :=
  iSup_subtype'

Bounded Union Equals Indexed Union

Informal description

For any set $s$ of type $\alpha$ and any family of sets $t$ indexed by elements $x \in s$ with values in $\beta$, the bounded union $\bigcup_{x \in s} t(x)$ is equal to the union $\bigcup_{x : s} t(x)$ where $x$ ranges over all elements of $s$.

Set.biInter_eq_iInter theorem

(s : Set α) (t : ∀ x ∈ s, Set β) : ⋂ x ∈ s, t x ‹_› = ⋂ x : s, t x x.2

Full source

theorem biInter_eq_iInter (s : Set α) (t : ∀ x ∈ s, Set β) :
    ⋂ x ∈ s, t x ‹_› = ⋂ x : s, t x x.2 :=
  iInf_subtype'

Bounded Intersection Equals Indexed Intersection

Informal description

For any set $s$ of type $\alpha$ and any family of sets $t$ indexed by elements $x \in s$ (where each $t(x)$ is a set of type $\beta$), the bounded intersection $\bigcap_{x \in s} t(x)$ is equal to the intersection $\bigcap_{x : s} t(x, h_x)$, where $h_x$ is a proof that $x \in s$.

Set.biUnion_const theorem

{s : Set α} (hs : s.Nonempty) (t : Set β) : ⋃ a ∈ s, t = t

Full source

@[simp] lemma biUnion_const {s : Set α} (hs : s.Nonempty) (t : Set β) : ⋃ a ∈ s, t = t :=
  biSup_const hs

Union of Constant Set over Nonempty Index Set Equals the Set

Informal description

For any nonempty set $s \subseteq \alpha$ and any set $t \subseteq \beta$, the union of $t$ over all elements in $s$ equals $t$ itself. In other words: $$\bigcup_{a \in s} t = t$$

Set.biInter_const theorem

{s : Set α} (hs : s.Nonempty) (t : Set β) : ⋂ a ∈ s, t = t

Full source

@[simp] lemma biInter_const {s : Set α} (hs : s.Nonempty) (t : Set β) : ⋂ a ∈ s, t = t :=
  biInf_const hs

Intersection over Nonempty Index Set Equals Target Set

Informal description

For any nonempty set $s$ of type $\alpha$ and any set $t$ of type $\beta$, the intersection of $t$ over all elements $a \in s$ equals $t$ itself, i.e., $\bigcap_{a \in s} t = t$.

Set.iUnion_subtype theorem

(p : α → Prop) (s : { x // p x } → Set β) : ⋃ x : { x // p x }, s x = ⋃ (x) (hx : p x), s ⟨x, hx⟩

Full source

theorem iUnion_subtype (p : α → Prop) (s : { x // p x } → Set β) :
    ⋃ x : { x // p x }, s x = ⋃ (x) (hx : p x), s ⟨x, hx⟩ :=
  iSup_subtype

Union over Subtype Equals Bounded Union

Informal description

For any predicate $p$ on a type $\alpha$ and any family of sets $s$ indexed by the subtype $\{x \mid p(x)\}$, the union of all sets $s(x)$ over $x$ in the subtype is equal to the union of all sets $s(\langle x, hx \rangle)$ over all $x \in \alpha$ satisfying $p(x)$. In symbols: \[ \bigcup_{x \in \{x \mid p(x)\}} s(x) = \bigcup_{x \in \alpha, hx : p(x)} s(\langle x, hx \rangle). \]

Set.iInter_subtype theorem

(p : α → Prop) (s : { x // p x } → Set β) : ⋂ x : { x // p x }, s x = ⋂ (x) (hx : p x), s ⟨x, hx⟩

Full source

theorem iInter_subtype (p : α → Prop) (s : { x // p x } → Set β) :
    ⋂ x : { x // p x }, s x = ⋂ (x) (hx : p x), s ⟨x, hx⟩ :=
  iInf_subtype

Intersection over Subtype Equals Bounded Intersection

Informal description

For any predicate $p$ on a type $\alpha$ and any family of sets $s$ indexed by the subtype $\{x \mid p(x)\}$, the intersection $\bigcap_{x : \{x \mid p(x)\}} s(x)$ is equal to the intersection $\bigcap_{x \in \alpha, hx : p(x)} s(\langle x, hx\rangle)$.

Set.biInter_empty theorem

(u : α → Set β) : ⋂ x ∈ (∅ : Set α), u x = univ

Full source

theorem biInter_empty (u : α → Set β) : ⋂ x ∈ (∅ : Set α), u x = univ :=
  iInf_emptyset

Intersection over Empty Set is Universal Set

Informal description

For any family of sets $u$ indexed by elements of a type $\alpha$, the intersection $\bigcap_{x \in \emptyset} u(x)$ over the empty set is equal to the universal set $\text{univ}$.

Set.biInter_univ theorem

(u : α → Set β) : ⋂ x ∈ @univ α, u x = ⋂ x, u x

Full source

theorem biInter_univ (u : α → Set β) : ⋂ x ∈ @univ α, u x = ⋂ x, u x :=
  iInf_univ

Bounded Intersection over Universal Set Equals Unbounded Intersection

Informal description

For any family of sets $u : \alpha \to \text{Set} \beta$, the bounded intersection over all $x$ in the universal set $\text{univ} : \text{Set} \alpha$ is equal to the unbounded intersection over all $x : \alpha$, i.e., \[ \bigcap_{x \in \text{univ}} u(x) = \bigcap_{x} u(x). \]

Set.biUnion_self theorem

(s : Set α) : ⋃ x ∈ s, s = s

Full source

@[simp]
theorem biUnion_self (s : Set α) : ⋃ x ∈ s, s = s :=
  Subset.antisymm (iUnion₂_subset fun _ _ => Subset.refl s) fun _ hx => mem_biUnion hx hx

Union over Set Equals Itself: $\bigcup_{x \in s} s = s$

Informal description

For any set $s$ of type $\alpha$, the union $\bigcup_{x \in s} s$ over all elements $x$ in $s$ is equal to $s$ itself.

Set.iUnion_nonempty_self theorem

(s : Set α) : ⋃ _ : s.Nonempty, s = s

Full source

@[simp]
theorem iUnion_nonempty_self (s : Set α) : ⋃ _ : s.Nonempty, s = s := by
  rw [iUnion_nonempty_index, biUnion_self]

Union over Nonempty Condition Equals Set Itself

Informal description

For any set $s$ of type $\alpha$, the union of $s$ over all proofs that $s$ is nonempty is equal to $s$ itself, i.e., $\bigcup_{\_ : s \text{ is nonempty}} s = s$.

Set.biInter_singleton theorem

(a : α) (s : α → Set β) : ⋂ x ∈ ({ a } : Set α), s x = s a

Full source

theorem biInter_singleton (a : α) (s : α → Set β) : ⋂ x ∈ ({a} : Set α), s x = s a :=
  iInf_singleton

Intersection over Singleton Set Equals Function Value

Informal description

For any element $a$ of type $\alpha$ and any function $s$ from $\alpha$ to sets of type $\beta$, the intersection of all sets $s(x)$ where $x$ belongs to the singleton set $\{a\}$ is equal to $s(a)$. In other words, $\bigcap_{x \in \{a\}} s(x) = s(a)$.

Set.biInter_union theorem

(s t : Set α) (u : α → Set β) : ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x

Full source

theorem biInter_union (s t : Set α) (u : α → Set β) :
    ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x :=
  iInf_union

Intersection over Union of Two Sets Equals Intersection of Intersections

Informal description

For any sets $s, t \subseteq \alpha$ and any family of sets $u : \alpha \to \text{Set } \beta$, the intersection over $x \in s \cup t$ of $u(x)$ is equal to the intersection of the intersection over $x \in s$ of $u(x)$ and the intersection over $x \in t$ of $u(x)$. In symbols: \[ \bigcap_{x \in s \cup t} u(x) = \left(\bigcap_{x \in s} u(x)\right) \cap \left(\bigcap_{x \in t} u(x)\right). \]

Set.biInter_insert theorem

(a : α) (s : Set α) (t : α → Set β) : ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

Full source

theorem biInter_insert (a : α) (s : Set α) (t : α → Set β) :
    ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x := by simp

Intersection over Inserted Set Equals Intersection with Singleton

Informal description

For any element $a$ of type $\alpha$, any set $s \subseteq \alpha$, and any family of sets $t : \alpha \to \text{Set } \beta$, the intersection over all $x$ in the set $\{a\} \cup s$ of $t(x)$ is equal to the intersection of $t(a)$ with the intersection over all $x \in s$ of $t(x)$. In symbols: \[ \bigcap_{x \in \{a\} \cup s} t(x) = t(a) \cap \left(\bigcap_{x \in s} t(x)\right). \]

Set.biInter_pair theorem

(a b : α) (s : α → Set β) : ⋂ x ∈ ({ a, b } : Set α), s x = s a ∩ s b

Full source

theorem biInter_pair (a b : α) (s : α → Set β) : ⋂ x ∈ ({a, b} : Set α), s x = s a ∩ s b := by
  rw [biInter_insert, biInter_singleton]

Intersection over Pair Equals Pairwise Intersection

Informal description

For any two elements $a$ and $b$ of type $\alpha$ and any family of sets $s : \alpha \to \text{Set } \beta$, the intersection of all sets $s(x)$ where $x$ belongs to the doubleton set $\{a, b\}$ is equal to the intersection of $s(a)$ and $s(b)$. In symbols: \[ \bigcap_{x \in \{a, b\}} s(x) = s(a) \cap s(b). \]

Set.biInter_inter theorem

 {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) : ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Full source

theorem biInter_inter {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) :
    ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t := by
  haveI : Nonempty s := hs.to_subtype
  simp [biInter_eq_iInter, ← iInter_inter]

Intersection of Intersections with a Fixed Set

Informal description

For any nonempty set $s$ of type $\iota$, any family of sets $f : \iota \to \text{Set} \alpha$, and any set $t$ of type $\alpha$, the intersection of the sets $f(i) \cap t$ over all $i \in s$ is equal to the intersection of the sets $f(i)$ over all $i \in s$, intersected with $t$. In symbols: \[ \bigcap_{i \in s} (f(i) \cap t) = \left(\bigcap_{i \in s} f(i)\right) \cap t. \]

Set.inter_biInter theorem

 {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) : ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

Full source

theorem inter_biInter {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) :
    ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i := by
  rw [inter_comm, ← biInter_inter hs]
  simp [inter_comm]

Intersection Commutes with Bounded Intersection

Informal description

For any nonempty set $s$ of type $\iota$, any family of sets $f : \iota \to \text{Set} \alpha$, and any set $t$ of type $\alpha$, the intersection of the sets $t \cap f(i)$ over all $i \in s$ is equal to $t$ intersected with the intersection of the sets $f(i)$ over all $i \in s$. In symbols: \[ \bigcap_{i \in s} (t \cap f(i)) = t \cap \left(\bigcap_{i \in s} f(i)\right). \]

Set.biUnion_empty theorem

(s : α → Set β) : ⋃ x ∈ (∅ : Set α), s x = ∅

Full source

theorem biUnion_empty (s : α → Set β) : ⋃ x ∈ (∅ : Set α), s x = ∅ :=
  iSup_emptyset

Union over Empty Set is Empty

Informal description

For any family of sets $s : \alpha \to \text{Set} \beta$, the union of all sets $s(x)$ where $x$ ranges over the empty set is equal to the empty set. In symbols: \[ \bigcup_{x \in \emptyset} s(x) = \emptyset. \]

Set.biUnion_univ theorem

(s : α → Set β) : ⋃ x ∈ @univ α, s x = ⋃ x, s x

Full source

theorem biUnion_univ (s : α → Set β) : ⋃ x ∈ @univ α, s x = ⋃ x, s x :=
  iSup_univ

Union over Universal Set Equals Unbounded Union

Informal description

For any family of sets $s : \alpha \to \text{Set} \beta$, the union of all sets $s(x)$ where $x$ ranges over the universal set $\text{univ} \alpha$ is equal to the union of all sets $s(x)$. In symbols: \[ \bigcup_{x \in \text{univ} \alpha} s(x) = \bigcup_{x} s(x). \]

Set.biUnion_singleton theorem

(a : α) (s : α → Set β) : ⋃ x ∈ ({ a } : Set α), s x = s a

Full source

theorem biUnion_singleton (a : α) (s : α → Set β) : ⋃ x ∈ ({a} : Set α), s x = s a :=
  iSup_singleton

Union over Singleton Set Equals Its Element's Image

Informal description

For any element $a$ of type $\alpha$ and any family of sets $s : \alpha \to \text{Set} \beta$, the union of all sets $s(x)$ where $x$ ranges over the singleton set $\{a\}$ is equal to $s(a)$. In symbols: \[ \bigcup_{x \in \{a\}} s(x) = s(a). \]

Set.biUnion_of_singleton theorem

(s : Set α) : ⋃ x ∈ s, { x } = s

Full source

@[simp]
theorem biUnion_of_singleton (s : Set α) : ⋃ x ∈ s, {x} = s :=
  ext <| by simp

Union of Singletons Equals Original Set

Informal description

For any set $s$ of elements of type $\alpha$, the union of all singleton sets $\{x\}$ for $x \in s$ equals $s$ itself, i.e., $$\bigcup_{x \in s} \{x\} = s.$$

Set.biUnion_union theorem

(s t : Set α) (u : α → Set β) : ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x

Full source

theorem biUnion_union (s t : Set α) (u : α → Set β) :
    ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x :=
  iSup_union

Union over Union Equals Union of Unions

Informal description

For any sets $s, t \subseteq \alpha$ and any family of sets $u : \alpha \to \text{Set } \beta$, the union of $u(x)$ over all $x \in s \cup t$ is equal to the union of the union of $u(x)$ over all $x \in s$ and the union of $u(x)$ over all $x \in t$. In symbols: \[ \bigcup_{x \in s \cup t} u(x) = \left(\bigcup_{x \in s} u(x)\right) \cup \left(\bigcup_{x \in t} u(x)\right). \]

Set.iUnion_coe_set theorem

{α β : Type*} (s : Set α) (f : s → Set β) : ⋃ i, f i = ⋃ i ∈ s, f ⟨i, ‹i ∈ s›⟩

Full source

@[simp]
theorem iUnion_coe_set {α β : Type*} (s : Set α) (f : s → Set β) :
    ⋃ i, f i = ⋃ i ∈ s, f ⟨i, ‹i ∈ s›⟩ :=
  iUnion_subtype _ _

Union over Subset Equals Union over Subtype Elements

Informal description

For any sets $s \subseteq \alpha$ and any family of sets $f$ indexed by elements of $s$, the union of all sets $f(i)$ over $i \in s$ is equal to the union of all sets $f(\langle i, h_i \rangle)$ over all $i \in s$, where $h_i$ is a proof that $i \in s$. In symbols: \[ \bigcup_{i \in s} f(i) = \bigcup_{i \in s} f(\langle i, h_i \rangle). \]

Set.iInter_coe_set theorem

{α β : Type*} (s : Set α) (f : s → Set β) : ⋂ i, f i = ⋂ i ∈ s, f ⟨i, ‹i ∈ s›⟩

Full source

@[simp]
theorem iInter_coe_set {α β : Type*} (s : Set α) (f : s → Set β) :
    ⋂ i, f i = ⋂ i ∈ s, f ⟨i, ‹i ∈ s›⟩ :=
  iInter_subtype _ _

Intersection over Set Equals Bounded Intersection over Elements

Informal description

For any sets $s \subseteq \alpha$ and any family of sets $f$ indexed by elements of $s$, the intersection $\bigcap_{i \in s} f(i)$ is equal to the intersection $\bigcap_{i \in s} f(\langle i, \text{proof of } i \in s \rangle)$.

Set.biUnion_insert theorem

(a : α) (s : Set α) (t : α → Set β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

Full source

theorem biUnion_insert (a : α) (s : Set α) (t : α → Set β) :
    ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x := by simp

Union over Inserted Set Equals Union of Singleton and Union over Original Set

Informal description

For any element $a \in \alpha$, any set $s \subseteq \alpha$, and any family of sets $t : \alpha \to \text{Set } \beta$, the union of all sets $t(x)$ for $x$ in the set $\{a\} \cup s$ equals the union of $t(a)$ with the union of all $t(x)$ for $x \in s$. In symbols: $$ \bigcup_{x \in \{a\} \cup s} t(x) = t(a) \cup \left( \bigcup_{x \in s} t(x) \right). $$

Set.biUnion_pair theorem

(a b : α) (s : α → Set β) : ⋃ x ∈ ({ a, b } : Set α), s x = s a ∪ s b

Full source

theorem biUnion_pair (a b : α) (s : α → Set β) : ⋃ x ∈ ({a, b} : Set α), s x = s a ∪ s b := by
  simp

Union over Pair Equals Pairwise Union

Informal description

For any two elements $a$ and $b$ of a type $\alpha$ and any family of sets $s : \alpha \to \text{Set } \beta$, the union of all sets $s(x)$ for $x$ in the pair $\{a, b\}$ equals the union of $s(a)$ and $s(b)$. In symbols: $$ \bigcup_{x \in \{a, b\}} s(x) = s(a) \cup s(b). $$

Set.inter_iUnion₂ theorem

(s : Set α) (t : ∀ i, κ i → Set α) : (s ∩ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ∩ t i j

Full source

theorem inter_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) :
    (s ∩ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ∩ t i j := by simp only [inter_iUnion]

Distributivity of Intersection over Double Union of Sets

Informal description

For any set $s$ in a type $\alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$, the intersection of $s$ with the double union of the $t_{i,j}$ equals the double union of the intersections of $s$ with each $t_{i,j}$. In symbols: $$ s \cap \left( \bigcup_{i} \bigcup_{j} t_{i,j} \right) = \bigcup_{i} \bigcup_{j} (s \cap t_{i,j}). $$

Set.iUnion₂_inter theorem

(s : ∀ i, κ i → Set α) (t : Set α) : (⋃ (i) (j), s i j) ∩ t = ⋃ (i) (j), s i j ∩ t

Full source

theorem iUnion₂_inter (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋃ (i) (j), s i j) ∩ t = ⋃ (i) (j), s i j ∩ t := by simp_rw [iUnion_inter]

Distributivity of Double Union over Intersection of Sets

Informal description

For any family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the intersection of the double union of the $s_{i,j}$ with $t$ equals the double union of the intersections of each $s_{i,j}$ with $t$. In symbols: $$ \left( \bigcup_{i} \bigcup_{j} s_{i,j} \right) \cap t = \bigcup_{i} \bigcup_{j} (s_{i,j} \cap t). $$

Set.union_iInter₂ theorem

(s : Set α) (t : ∀ i, κ i → Set α) : (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j

Full source

theorem union_iInter₂ (s : Set α) (t : ∀ i, κ i → Set α) :
    (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j := by simp_rw [union_iInter]

Distributivity of Union over Double Intersection

Informal description

For any set $s$ in a type $\alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \iota, j \in \kappa_i}$, the union of $s$ with the intersection of all $t_{i,j}$ equals the intersection of all unions $s \cup t_{i,j}$. That is, $$ s \cup \left( \bigcap_{i} \bigcap_{j} t_{i,j} \right) = \bigcap_{i} \bigcap_{j} (s \cup t_{i,j}). $$

Set.iInter₂_union theorem

(s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t

Full source

theorem iInter₂_union (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t := by simp_rw [iInter_union]

Distributivity of Union over Double Intersection for Indexed Family of Sets

Informal description

For any family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the union of the double intersection of the $s_{i,j}$ with $t$ equals the double intersection of the unions of each $s_{i,j}$ with $t$. In symbols: $$\left( \bigcap_{i} \bigcap_{j} s_{i,j} \right) \cup t = \bigcap_{i} \bigcap_{j} (s_{i,j} \cup t).$$

Set.mem_sUnion_of_mem theorem

{x : α} {t : Set α} {S : Set (Set α)} (hx : x ∈ t) (ht : t ∈ S) : x ∈ ⋃₀ S

Full source

theorem mem_sUnion_of_mem {x : α} {t : Set α} {S : Set (Set α)} (hx : x ∈ t) (ht : t ∈ S) :
    x ∈ ⋃₀ S :=
  ⟨t, ht, hx⟩

Element in Union of Collection via Member Set

Informal description

For any element $x$ in a type $\alpha$, any set $t \subseteq \alpha$, and any collection $S$ of subsets of $\alpha$, if $x \in t$ and $t \in S$, then $x$ belongs to the union of all sets in $S$, denoted $\bigcup S$.

Set.not_mem_of_not_mem_sUnion theorem

{x : α} {t : Set α} {S : Set (Set α)} (hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t

Full source

theorem not_mem_of_not_mem_sUnion {x : α} {t : Set α} {S : Set (Set α)} (hx : x ∉ ⋃₀ S)
    (ht : t ∈ S) : x ∉ t := fun h => hx ⟨t, ht, h⟩

Non-membership in Union Implies Non-membership in Member Set

Informal description

For any element $x$ of type $\alpha$, any set $t$ of type $\alpha$, and any collection $S$ of sets of type $\alpha$, if $x$ is not in the union of all sets in $S$ and $t$ is a member of $S$, then $x$ is not in $t$.

Set.sInter_subset_of_mem theorem

{S : Set (Set α)} {t : Set α} (tS : t ∈ S) : ⋂₀ S ⊆ t

Full source

theorem sInter_subset_of_mem {S : Set (Set α)} {t : Set α} (tS : t ∈ S) : ⋂₀ S⋂₀ S ⊆ t :=
  sInf_le tS

Intersection of Family is Subset of Member Set

Informal description

For any family of sets $S$ in a type $\alpha$ and any set $t \in S$, the intersection of all sets in $S$ is a subset of $t$, i.e., $\bigcap_{s \in S} s \subseteq t$.

Set.subset_sUnion_of_mem theorem

{S : Set (Set α)} {t : Set α} (tS : t ∈ S) : t ⊆ ⋃₀ S

Full source

theorem subset_sUnion_of_mem {S : Set (Set α)} {t : Set α} (tS : t ∈ S) : t ⊆ ⋃₀ S :=
  le_sSup tS

Set in Family is Subset of its Union

Informal description

For any family of sets $S$ and any set $t \in S$, we have $t \subseteq \bigcup S$.

Set.subset_sUnion_of_subset theorem

{s : Set α} (t : Set (Set α)) (u : Set α) (h₁ : s ⊆ u) (h₂ : u ∈ t) : s ⊆ ⋃₀ t

Full source

theorem subset_sUnion_of_subset {s : Set α} (t : Set (Set α)) (u : Set α) (h₁ : s ⊆ u)
    (h₂ : u ∈ t) : s ⊆ ⋃₀ t :=
  Subset.trans h₁ (subset_sUnion_of_mem h₂)

Subset Propagation to Union via Intermediate Set

Informal description

For any set $s$ in a type $\alpha$, any family of sets $t$ in $\alpha$, and any set $u \in t$, if $s$ is a subset of $u$, then $s$ is also a subset of the union of all sets in $t$, i.e., $s \subseteq \bigcup t$.

Set.sUnion_subset theorem

{S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t' ⊆ t) : ⋃₀ S ⊆ t

Full source

theorem sUnion_subset {S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t' ⊆ t) : ⋃₀ S⋃₀ S ⊆ t :=
  sSup_le h

Union of Subsets is Subset

Informal description

For any collection of sets $S$ in a type $\alpha$ and any set $t \subseteq \alpha$, if every set $t' \in S$ satisfies $t' \subseteq t$, then the union of all sets in $S$ is also contained in $t$, i.e., $\bigcup_{t' \in S} t' \subseteq t$.

Set.sUnion_subset_iff theorem

{s : Set (Set α)} {t : Set α} : ⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t

Full source

@[simp]
theorem sUnion_subset_iff {s : Set (Set α)} {t : Set α} : ⋃₀ s⋃₀ s ⊆ t⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t :=
  sSup_le_iff

Characterization of Union Subset via Member Subsets

Informal description

For a family of sets $s$ in a type $\alpha$ and a set $t \subseteq \alpha$, the union of all sets in $s$ is contained in $t$ if and only if every set $t'$ in $s$ is contained in $t$. In symbols: \[ \bigcup₀ s \subseteq t \leftrightarrow \forall t' \in s, t' \subseteq t \]

Set.sUnion_mono_subsets theorem

{s : Set (Set α)} {f : Set α → Set α} (hf : ∀ t : Set α, t ⊆ f t) : ⋃₀ s ⊆ ⋃₀ (f '' s)

Full source

/-- `sUnion` is monotone under taking a subset of each set. -/
lemma sUnion_mono_subsets {s : Set (Set α)} {f : Set α → Set α} (hf : ∀ t : Set α, t ⊆ f t) :
    ⋃₀ s⋃₀ s ⊆ ⋃₀ (f '' s) :=
  fun _ ⟨t, htx, hxt⟩ ↦ ⟨f t, mem_image_of_mem f htx, hf t hxt⟩

Monotonicity of Union under Set Expansion

Informal description

For any family of sets $s$ in a type $\alpha$ and any function $f : \text{Set } \alpha \to \text{Set } \alpha$ such that $t \subseteq f(t)$ for all $t \in \text{Set } \alpha$, the union of all sets in $s$ is contained in the union of the images of all sets in $s$ under $f$. In symbols: \[ \bigcup_{t \in s} t \subseteq \bigcup_{t \in s} f(t). \]

Set.sUnion_mono_supsets theorem

{s : Set (Set α)} {f : Set α → Set α} (hf : ∀ t : Set α, f t ⊆ t) : ⋃₀ (f '' s) ⊆ ⋃₀ s

Full source

/-- `sUnion` is monotone under taking a superset of each set. -/
lemma sUnion_mono_supsets {s : Set (Set α)} {f : Set α → Set α} (hf : ∀ t : Set α, f t ⊆ t) :
    ⋃₀ (f '' s)⋃₀ (f '' s) ⊆ ⋃₀ s :=
  -- If t ∈ f '' s is arbitrary; t = f u for some u : Set α.
  fun _ ⟨_, ⟨u, hus, hut⟩, hxt⟩ ↦ ⟨u, hus, (hut ▸ hf u) hxt⟩

Union of Subsets is Contained in Original Union

Informal description

For any family of sets $s$ in a type $\alpha$ and any function $f : \text{Set } \alpha \to \text{Set } \alpha$ such that $f(t) \subseteq t$ for every set $t$, the union of the image of $s$ under $f$ is contained in the union of $s$, i.e., $\bigcup_{t \in s} f(t) \subseteq \bigcup_{t \in s} t$.

Set.subset_sInter theorem

{S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t ⊆ t') : t ⊆ ⋂₀ S

Full source

theorem subset_sInter {S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t ⊆ t') : t ⊆ ⋂₀ S :=
  le_sInf h

Subset of Intersection via Universal Subset Condition

Informal description

For any family of sets $S$ in a type $\alpha$ and any set $t \subseteq \alpha$, if $t$ is a subset of every set $t' \in S$, then $t$ is a subset of the intersection $\bigcap_{t' \in S} t'$.

Set.subset_sInter_iff theorem

{S : Set (Set α)} {t : Set α} : t ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t'

Full source

@[simp]
theorem subset_sInter_iff {S : Set (Set α)} {t : Set α} : t ⊆ ⋂₀ St ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t' :=
  le_sInf_iff

Characterization of Subset of Set Intersection: $t \subseteq \bigcap₀ S \leftrightarrow \forall t' \in S, t \subseteq t'$

Informal description

For any family of sets $S$ and any set $t$, the set $t$ is contained in the intersection $\bigcap₀ S$ of all sets in $S$ if and only if $t$ is contained in every set $t' \in S$.

Set.sUnion_subset_sUnion theorem

{S T : Set (Set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T

Full source

@[gcongr]
theorem sUnion_subset_sUnion {S T : Set (Set α)} (h : S ⊆ T) : ⋃₀ S⋃₀ S ⊆ ⋃₀ T :=
  sUnion_subset fun _ hs => subset_sUnion_of_mem (h hs)

Monotonicity of Union with Respect to Family Inclusion

Informal description

For any two families of sets $S$ and $T$ in a type $\alpha$, if $S$ is a subset of $T$, then the union of all sets in $S$ is contained in the union of all sets in $T$, i.e., $\bigcup₀ S \subseteq \bigcup₀ T$.

Set.sInter_subset_sInter theorem

{S T : Set (Set α)} (h : S ⊆ T) : ⋂₀ T ⊆ ⋂₀ S

Full source

@[gcongr]
theorem sInter_subset_sInter {S T : Set (Set α)} (h : S ⊆ T) : ⋂₀ T⋂₀ T ⊆ ⋂₀ S :=
  subset_sInter fun _ hs => sInter_subset_of_mem (h hs)

Antitonicity of Set Intersection with Respect to Family Inclusion

Informal description

For any two families of sets $S$ and $T$ in a type $\alpha$, if $S \subseteq T$, then the intersection of all sets in $T$ is a subset of the intersection of all sets in $S$, i.e., $\bigcap_{t \in T} t \subseteq \bigcap_{s \in S} s$.

Set.sUnion_empty theorem

: ⋃₀ ∅ = (∅ : Set α)

Full source

@[simp]
theorem sUnion_empty : ⋃₀ ∅ = (∅ : Set α) :=
  sSup_empty

Union of Empty Family is Empty Set

Informal description

The union of an empty family of sets is the empty set, i.e., $\bigcup₀ \emptyset = \emptyset$.

Set.sInter_empty theorem

: ⋂₀ ∅ = (univ : Set α)

Full source

@[simp]
theorem sInter_empty : ⋂₀ ∅ = (univ : Set α) :=
  sInf_empty

Intersection of Empty Family is Universal Set

Informal description

The intersection of an empty family of sets in a type $\alpha$ is equal to the universal set $\text{univ} : \text{Set } \alpha$.

Set.sUnion_singleton theorem

(s : Set α) : ⋃₀ { s } = s

Full source

@[simp]
theorem sUnion_singleton (s : Set α) : ⋃₀ {s} = s :=
  sSup_singleton

Union of Singleton Set Equals Itself

Informal description

For any set $s$ in a type $\alpha$, the union of the singleton collection $\{s\}$ is equal to $s$ itself, i.e., $\bigcup \{s\} = s$.

Set.sInter_singleton theorem

(s : Set α) : ⋂₀ { s } = s

Full source

@[simp]
theorem sInter_singleton (s : Set α) : ⋂₀ {s} = s :=
  sInf_singleton

Intersection of Singleton Set is the Set Itself

Informal description

For any set $s$ in a type $\alpha$, the intersection of the singleton collection $\{s\}$ is equal to $s$ itself, i.e., $\bigcap₀ \{s\} = s$.

Set.sUnion_eq_empty theorem

{S : Set (Set α)} : ⋃₀ S = ∅ ↔ ∀ s ∈ S, s = ∅

Full source

@[simp]
theorem sUnion_eq_empty {S : Set (Set α)} : ⋃₀ S⋃₀ S = ∅ ↔ ∀ s ∈ S, s = ∅ :=
  sSup_eq_bot

Union of a Family of Sets is Empty if and only if All Sets are Empty

Informal description

For a family of sets $S$ in a type $\alpha$, the union of all sets in $S$ is empty if and only if every set in $S$ is empty, i.e., \[ \bigcup_{s \in S} s = \emptyset \leftrightarrow \forall s \in S, s = \emptyset. \]

Set.sInter_eq_univ theorem

{S : Set (Set α)} : ⋂₀ S = univ ↔ ∀ s ∈ S, s = univ

Full source

@[simp]
theorem sInter_eq_univ {S : Set (Set α)} : ⋂₀ S⋂₀ S = univ ↔ ∀ s ∈ S, s = univ :=
  sInf_eq_top

Intersection Equals Universal Set iff All Sets are Universal

Informal description

For a family of sets $S$ in a type $\alpha$, the intersection of all sets in $S$ equals the universal set $\alpha$ if and only if every set $s$ in $S$ is equal to the universal set. In symbols: \[ \bigcap_{s \in S} s = \alpha \leftrightarrow \forall s \in S, s = \alpha. \]

Set.subset_powerset_iff theorem

{s : Set (Set α)} {t : Set α} : s ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t

Full source

theorem subset_powerset_iff {s : Set (Set α)} {t : Set α} : s ⊆ 𝒫 ts ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t :=
  sUnion_subset_iff.symm

Powerset Containment via Union Subset

Informal description

For a family of sets $s$ in a type $\alpha$ and a set $t \subseteq \alpha$, the family $s$ is contained in the powerset of $t$ if and only if the union of all sets in $s$ is contained in $t$. In symbols: \[ s \subseteq \mathcal{P}(t) \leftrightarrow \bigcup₀ s \subseteq t \]

Set.sUnion_powerset_gc theorem

: GaloisConnection (⋃₀ · : Set (Set α) → Set α) (𝒫· : Set α → Set (Set α))

Full source

/-- `⋃₀` and `𝒫` form a Galois connection. -/
theorem sUnion_powerset_gc :
    GaloisConnection (⋃₀ · : Set (Set α) → Set α) (𝒫 · : Set α → Set (Set α)) :=
  gc_sSup_Iic

Galois connection between union of sets and powerset

Informal description

The pair of functions $(\bigcup₀, \mathcal{P})$ forms a Galois connection between the complete lattice of sets of sets $\mathcal{P}(\mathcal{P}(\alpha))$ and the complete lattice of sets $\mathcal{P}(\alpha)$. Here $\bigcup₀$ denotes the union of a family of sets, and $\mathcal{P}$ denotes the powerset operation.

Set.sUnionPowersetGI definition

: GaloisInsertion (⋃₀ · : Set (Set α) → Set α) (𝒫· : Set α → Set (Set α))

Full source

/-- `⋃₀` and `𝒫` form a Galois insertion. -/
def sUnionPowersetGI :
    GaloisInsertion (⋃₀ · : Set (Set α) → Set α) (𝒫 · : Set α → Set (Set α)) :=
  gi_sSup_Iic

Galois insertion between set union and powerset

Informal description

The pair of operations consisting of set union ($\bigcup₀$) and powerset ($\mathcal{P}$) forms a Galois insertion between the complete lattice of sets of sets and the complete lattice of sets. Specifically, for any family of sets $S \subseteq \mathcal{P}(α)$ and any set $t \subseteq α$, we have $\bigcup₀ S \subseteq t$ if and only if $S \subseteq \mathcal{P}(t)$.

Set.sUnion_mem_empty_univ theorem

{S : Set (Set α)} (h : S ⊆ {∅, univ}) : ⋃₀ S ∈ ({∅, univ} : Set (Set α))

Full source

/-- If all sets in a collection are either `∅` or `Set.univ`, then so is their union. -/
theorem sUnion_mem_empty_univ {S : Set (Set α)} (h : S ⊆ {∅, univ}) :
    ⋃₀ S⋃₀ S ∈ ({∅, univ} : Set (Set α)) := by
  simp only [mem_insert_iff, mem_singleton_iff, or_iff_not_imp_left, sUnion_eq_empty, not_forall]
  rintro ⟨s, hs, hne⟩
  obtain rfl : s = univ := (h hs).resolve_left hne
  exact univ_subset_iff.1 <| subset_sUnion_of_mem hs

Union of Trivial Sets is Trivial

Informal description

For any collection of sets $S$ in a type $\alpha$, if every set in $S$ is either the empty set $\emptyset$ or the universal set $\text{univ}$, then their union $\bigcup S$ is also either $\emptyset$ or $\text{univ}$.

Set.nonempty_sUnion theorem

{S : Set (Set α)} : (⋃₀ S).Nonempty ↔ ∃ s ∈ S, Set.Nonempty s

Full source

@[simp]
theorem nonempty_sUnion {S : Set (Set α)} : (⋃₀ S).Nonempty ↔ ∃ s ∈ S, Set.Nonempty s := by
  simp [nonempty_iff_ne_empty]

Nonempty Union of Sets is Nonempty if and only if Some Member is Nonempty

Informal description

For any family of sets $S$ in a type $\alpha$, the union $\bigcup S$ is nonempty if and only if there exists some set $s \in S$ that is nonempty.

Set.Nonempty.of_sUnion theorem

{s : Set (Set α)} (h : (⋃₀ s).Nonempty) : s.Nonempty

Full source

theorem Nonempty.of_sUnion {s : Set (Set α)} (h : (⋃₀ s).Nonempty) : s.Nonempty :=
  let ⟨s, hs, _⟩ := nonempty_sUnion.1 h
  ⟨s, hs⟩

Nonempty Union Implies Nonempty Family of Sets

Informal description

For any family of sets $s$ in a type $\alpha$, if the union $\bigcup s$ is nonempty, then the family $s$ itself is nonempty.

Set.Nonempty.of_sUnion_eq_univ theorem

[Nonempty α] {s : Set (Set α)} (h : ⋃₀ s = univ) : s.Nonempty

Full source

theorem Nonempty.of_sUnion_eq_univ [Nonempty α] {s : Set (Set α)} (h : ⋃₀ s = univ) : s.Nonempty :=
  Nonempty.of_sUnion <| h.symm ▸ univ_nonempty

Nonempty Family from Full Union Cover

Informal description

Let $\alpha$ be a nonempty type and $s$ be a family of subsets of $\alpha$. If the union of all sets in $s$ equals the universal set $\alpha$, then the family $s$ is nonempty.

Set.sUnion_union theorem

(S T : Set (Set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T

Full source

theorem sUnion_union (S T : Set (Set α)) : ⋃₀ (S ∪ T) = ⋃₀ S⋃₀ S ∪ ⋃₀ T :=
  sSup_union

Union of Unions Equals Union of Union Components

Informal description

For any two collections of sets $S$ and $T$ in a type $\alpha$, the union of all sets in $S \cup T$ is equal to the union of all sets in $S$ combined with the union of all sets in $T$. In symbols: $$\bigcup (S \cup T) = \left(\bigcup S\right) \cup \left(\bigcup T\right)$$

Set.sInter_union theorem

(S T : Set (Set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T

Full source

theorem sInter_union (S T : Set (Set α)) : ⋂₀ (S ∪ T) = ⋂₀ S⋂₀ S ∩ ⋂₀ T :=
  sInf_union

Intersection of Union of Set Collections Equals Intersection of Intersections

Informal description

For any two collections of sets $S$ and $T$ in a type $\alpha$, the intersection of all sets in $S \cup T$ is equal to the intersection of all sets in $S$ intersected with the intersection of all sets in $T$. In symbols: $$\bigcap (S \cup T) = \left(\bigcap S\right) \cap \left(\bigcap T\right)$$

Set.sUnion_insert theorem

(s : Set α) (T : Set (Set α)) : ⋃₀ insert s T = s ∪ ⋃₀ T

Full source

@[simp]
theorem sUnion_insert (s : Set α) (T : Set (Set α)) : ⋃₀ insert s T = s ∪ ⋃₀ T :=
  sSup_insert

Union of Inserted Set Equals Union with Existing Union

Informal description

For any set $s$ in a type $\alpha$ and any collection of sets $T$ in $\alpha$, the union of all sets in the collection obtained by inserting $s$ into $T$ is equal to the union of $s$ with the union of all sets in $T$. In symbols: $$\bigcup (s \cup T) = s \cup \left(\bigcup T\right)$$

Set.sInter_insert theorem

(s : Set α) (T : Set (Set α)) : ⋂₀ insert s T = s ∩ ⋂₀ T

Full source

@[simp]
theorem sInter_insert (s : Set α) (T : Set (Set α)) : ⋂₀ insert s T = s ∩ ⋂₀ T :=
  sInf_insert

Intersection over Inserted Set Collection

Informal description

For any set $s$ in a type $\alpha$ and any collection of sets $T \subseteq \mathcal{P}(\alpha)$, the intersection of all sets in the collection formed by inserting $s$ into $T$ equals the intersection of $s$ with the intersection of all sets in $T$. In symbols: \[ \bigcap₀ (s \cup T) = s \cap \left(\bigcap₀ T\right) \]

Set.sUnion_diff_singleton_empty theorem

(s : Set (Set α)) : ⋃₀ (s \ {∅}) = ⋃₀ s

Full source

@[simp]
theorem sUnion_diff_singleton_empty (s : Set (Set α)) : ⋃₀ (s \ {∅}) = ⋃₀ s :=
  sSup_diff_singleton_bot s

Union of Sets Minus Empty Set Equals Union of All Sets

Informal description

For any family of sets $s$ in a type $\alpha$, the union of all sets in $s$ excluding the empty set is equal to the union of all sets in $s$. That is, $\bigcup (s \setminus \{\emptyset\}) = \bigcup s$.

Set.sInter_diff_singleton_univ theorem

(s : Set (Set α)) : ⋂₀ (s \ { univ }) = ⋂₀ s

Full source

@[simp]
theorem sInter_diff_singleton_univ (s : Set (Set α)) : ⋂₀ (s \ {univ}) = ⋂₀ s :=
  sInf_diff_singleton_top s

Intersection Unaffected by Removing Universal Set from Family

Informal description

For any family of sets $s$ in a type $\alpha$, the intersection of all sets in $s$ excluding the universal set equals the intersection of all sets in $s$. In other words, \[ \bigcap (s \setminus \{\text{univ}\}) = \bigcap s \] where $\text{univ}$ denotes the universal set containing all elements of type $\alpha$.

Set.sUnion_pair theorem

(s t : Set α) : ⋃₀ { s, t } = s ∪ t

Full source

theorem sUnion_pair (s t : Set α) : ⋃₀ {s, t} = s ∪ t :=
  sSup_pair

Union of Pair Equals Pairwise Union

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the union of the pair $\{s, t\}$ equals the union $s \cup t$. That is, $\bigcup \{s, t\} = s \cup t$.

Set.sInter_pair theorem

(s t : Set α) : ⋂₀ { s, t } = s ∩ t

Full source

theorem sInter_pair (s t : Set α) : ⋂₀ {s, t} = s ∩ t :=
  sInf_pair

Intersection of Pair of Sets Equals Pairwise Intersection

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the intersection of the collection $\{s, t\}$ equals the intersection of $s$ and $t$, i.e., \[ \bigcap \{s, t\} = s \cap t. \]

Set.sUnion_image theorem

(f : α → Set β) (s : Set α) : ⋃₀ (f '' s) = ⋃ a ∈ s, f a

Full source

@[simp]
theorem sUnion_image (f : α → Set β) (s : Set α) : ⋃₀ (f '' s) = ⋃ a ∈ s, f a :=
  sSup_image

Union of Image Equals Union of Function Values

Informal description

For any function $f \colon \alpha \to \mathcal{P}(\beta)$ and any set $s \subseteq \alpha$, the union of the image of $s$ under $f$ equals the union of $f(a)$ over all $a \in s$. In symbols: \[ \bigcup_{x \in f''s} x = \bigcup_{a \in s} f(a) \]

Set.sInter_image theorem

(f : α → Set β) (s : Set α) : ⋂₀ (f '' s) = ⋂ a ∈ s, f a

Full source

@[simp]
theorem sInter_image (f : α → Set β) (s : Set α) : ⋂₀ (f '' s) = ⋂ a ∈ s, f a :=
  sInf_image

Intersection of Image Equals Intersection over Original Set

Informal description

For any function $f \colon \alpha \to \mathcal{P}(\beta)$ and any subset $s \subseteq \alpha$, the intersection of the image of $s$ under $f$ is equal to the intersection of $f(a)$ over all $a \in s$. That is, \[ \bigcap_{x \in f''s} x = \bigcap_{a \in s} f(a). \]

Set.sUnion_image2 theorem

(f : α → β → Set γ) (s : Set α) (t : Set β) : ⋃₀ (image2 f s t) = ⋃ (a ∈ s) (b ∈ t), f a b

Full source

@[simp]
lemma sUnion_image2 (f : α → β → Set γ) (s : Set α) (t : Set β) :
    ⋃₀ (image2 f s t) = ⋃ (a ∈ s) (b ∈ t), f a b := sSup_image2

Union of Image2 Equals Bounded Union of Function Values

Informal description

For any function $f \colon \alpha \to \beta \to \text{Set } \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the union of the image of $f$ over $s \times t$ equals the union of $f(a,b)$ for all $a \in s$ and $b \in t$. In symbols: \[ \bigcup₀ \text{image2 } f \, s \, t = \bigcup_{\substack{a \in s \\ b \in t}} f(a, b). \]

Set.sInter_image2 theorem

(f : α → β → Set γ) (s : Set α) (t : Set β) : ⋂₀ (image2 f s t) = ⋂ (a ∈ s) (b ∈ t), f a b

Full source

@[simp]
lemma sInter_image2 (f : α → β → Set γ) (s : Set α) (t : Set β) :
    ⋂₀ (image2 f s t) = ⋂ (a ∈ s) (b ∈ t), f a b := sInf_image2

Intersection of Image under Binary Function Equals Bounded Intersection

Informal description

For any function $f : \alpha \to \beta \to \text{Set } \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the intersection of the image of $s$ and $t$ under $f$ equals the intersection of all $f(a,b)$ where $a \in s$ and $b \in t$. That is, \[ \bigcap₀ (f '' (s \times t)) = \bigcap_{a \in s, b \in t} f(a,b). \]

Set.sUnion_range theorem

(f : ι → Set β) : ⋃₀ range f = ⋃ x, f x

Full source

@[simp]
theorem sUnion_range (f : ι → Set β) : ⋃₀ range f = ⋃ x, f x :=
  rfl

Union of Range Equals Indexed Union

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ indexed by a type $\iota$, the union of all sets in the range of $f$ equals the union of all $f_i$ over all $i \in \iota$. In symbols: $$\bigcup_{i \in \iota} f_i = \bigcup_{x \in \iota} f_x$$

Set.sInter_range theorem

(f : ι → Set β) : ⋂₀ range f = ⋂ x, f x

Full source

@[simp]
theorem sInter_range (f : ι → Set β) : ⋂₀ range f = ⋂ x, f x :=
  rfl

Intersection of Range Equals Indexed Intersection

Informal description

For any function $f$ mapping from a type $\iota$ to sets of type $\beta$, the intersection of all sets in the range of $f$ equals the intersection of $f(x)$ over all $x \in \iota$. In symbols: $$\bigcap₀ \text{range } f = \bigcap_{x} f(x)$$

Set.iUnion_eq_univ_iff theorem

{f : ι → Set α} : ⋃ i, f i = univ ↔ ∀ x, ∃ i, x ∈ f i

Full source

theorem iUnion_eq_univ_iff {f : ι → Set α} : ⋃ i, f i⋃ i, f i = univ ↔ ∀ x, ∃ i, x ∈ f i := by
  simp only [eq_univ_iff_forall, mem_iUnion]

Characterization of Union Equals Universal Set: $\bigcup_i f_i = \text{univ} \leftrightarrow \forall x, \exists i, x \in f_i$

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ in a type $\alpha$, the union $\bigcup_{i \in \iota} f_i$ equals the universal set $\text{univ}$ if and only if for every element $x \in \alpha$, there exists an index $i \in \iota$ such that $x \in f_i$.

Set.iUnion₂_eq_univ_iff theorem

{s : ∀ i, κ i → Set α} : ⋃ (i) (j), s i j = univ ↔ ∀ a, ∃ i j, a ∈ s i j

Full source

theorem iUnion₂_eq_univ_iff {s : ∀ i, κ i → Set α} :
    ⋃ (i) (j), s i j⋃ (i) (j), s i j = univ ↔ ∀ a, ∃ i j, a ∈ s i j := by
  simp only [iUnion_eq_univ_iff, mem_iUnion]

Characterization of Universal Set as Double Union of Indexed Family

Informal description

For a family of sets $\{s_{i,j}\}_{i,j}$ indexed by $i$ and $j$, the union of all sets in the family equals the universal set if and only if for every element $a$, there exist indices $i$ and $j$ such that $a \in s_{i,j}$.

Set.sUnion_eq_univ_iff theorem

{c : Set (Set α)} : ⋃₀ c = univ ↔ ∀ a, ∃ b ∈ c, a ∈ b

Full source

theorem sUnion_eq_univ_iff {c : Set (Set α)} : ⋃₀ c⋃₀ c = univ ↔ ∀ a, ∃ b ∈ c, a ∈ b := by
  simp only [eq_univ_iff_forall, mem_sUnion]

Union of Collection Equals Universal Set iff Every Element is in Some Member

Informal description

For a collection $c$ of subsets of a type $\alpha$, the union of all sets in $c$ equals the universal set $\text{univ}$ if and only if for every element $a \in \alpha$, there exists a set $b \in c$ such that $a \in b$.

Set.iInter_eq_empty_iff theorem

{f : ι → Set α} : ⋂ i, f i = ∅ ↔ ∀ x, ∃ i, x ∉ f i

Full source

theorem iInter_eq_empty_iff {f : ι → Set α} : ⋂ i, f i⋂ i, f i = ∅ ↔ ∀ x, ∃ i, x ∉ f i := by
  simp [Set.eq_empty_iff_forall_not_mem]

Empty Intersection Characterization for Indexed Family of Sets

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ in a type $\alpha$, the intersection $\bigcap_{i} f_i$ is empty if and only if for every element $x \in \alpha$, there exists an index $i$ such that $x \notin f_i$.

Set.iInter₂_eq_empty_iff theorem

{s : ∀ i, κ i → Set α} : ⋂ (i) (j), s i j = ∅ ↔ ∀ a, ∃ i j, a ∉ s i j

Full source

theorem iInter₂_eq_empty_iff {s : ∀ i, κ i → Set α} :
    ⋂ (i) (j), s i j⋂ (i) (j), s i j = ∅ ↔ ∀ a, ∃ i j, a ∉ s i j := by
  simp only [eq_empty_iff_forall_not_mem, mem_iInter, not_forall]

Empty Intersection Condition for Double-Indexed Family of Sets

Informal description

For a family of sets $\{s_{i,j}\}_{i,j}$ indexed by $i$ and $j$, the intersection $\bigcap_{i,j} s_{i,j}$ is empty if and only if for every element $a$, there exist indices $i$ and $j$ such that $a \notin s_{i,j}$.

Set.sInter_eq_empty_iff theorem

{c : Set (Set α)} : ⋂₀ c = ∅ ↔ ∀ a, ∃ b ∈ c, a ∉ b

Full source

theorem sInter_eq_empty_iff {c : Set (Set α)} : ⋂₀ c⋂₀ c = ∅ ↔ ∀ a, ∃ b ∈ c, a ∉ b := by
  simp [Set.eq_empty_iff_forall_not_mem]

Intersection of a Collection of Sets is Empty if and only if Every Element is Excluded from Some Set in the Collection

Informal description

For a collection of sets $c \subseteq \mathcal{P}(\alpha)$, the intersection of all sets in $c$ is empty if and only if for every element $a \in \alpha$, there exists a set $b \in c$ such that $a \notin b$. In symbols: \[ \bigcap₀ c = \emptyset \leftrightarrow \forall a, \exists b \in c, a \notin b. \]

Set.nonempty_iInter theorem

{f : ι → Set α} : (⋂ i, f i).Nonempty ↔ ∃ x, ∀ i, x ∈ f i

Full source

@[simp]
theorem nonempty_iInter {f : ι → Set α} : (⋂ i, f i).Nonempty ↔ ∃ x, ∀ i, x ∈ f i := by
  simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]

Nonempty Intersection Criterion for Indexed Family of Sets

Informal description

For a family of sets $\{f_i\}_{i \in \iota}$ indexed by $\iota$, the intersection $\bigcap_{i} f_i$ is nonempty if and only if there exists an element $x$ that belongs to every set $f_i$ in the family.

Set.nonempty_iInter₂ theorem

{s : ∀ i, κ i → Set α} : (⋂ (i) (j), s i j).Nonempty ↔ ∃ a, ∀ i j, a ∈ s i j

Full source

theorem nonempty_iInter₂ {s : ∀ i, κ i → Set α} :
    (⋂ (i) (j), s i j).Nonempty ↔ ∃ a, ∀ i j, a ∈ s i j := by
  simp

Nonemptiness of Double Intersection of Sets

Informal description

For a doubly indexed family of sets $\{s_{i,j}\}_{i,j}$ in a type $\alpha$, the intersection $\bigcap_{i,j} s_{i,j}$ is nonempty if and only if there exists an element $a \in \alpha$ that belongs to every set $s_{i,j}$ in the family, i.e., $\exists a, \forall i j, a \in s_{i,j}$.

Set.nonempty_sInter theorem

{c : Set (Set α)} : (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b

Full source

@[simp]
theorem nonempty_sInter {c : Set (Set α)} : (⋂₀ c).Nonempty ↔ ∃ a, ∀ b ∈ c, a ∈ b := by
  simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]

Nonemptiness of Set Intersection via Common Element

Informal description

For a family of sets $c$ in a type $\alpha$, the intersection $\bigcap₀ c$ is nonempty if and only if there exists an element $a \in \alpha$ that belongs to every set $b \in c$.

Set.compl_sUnion theorem

(S : Set (Set α)) : (⋃₀ S)ᶜ = ⋂₀ (compl '' S)

Full source

theorem compl_sUnion (S : Set (Set α)) : (⋃₀ S)ᶜ = ⋂₀ (compl '' S) :=
  ext fun x => by simp

De Morgan's Law for Set Union: Complement of Union Equals Intersection of Complements

Informal description

For any family of sets $S \subseteq \mathcal{P}(\alpha)$, the complement of the union $\bigcup_{X \in S} X$ is equal to the intersection of the complements of all sets in $S$. That is, \[ \left( \bigcup_{X \in S} X \right)^c = \bigcap_{X \in S} X^c. \]

Set.sUnion_eq_compl_sInter_compl theorem

(S : Set (Set α)) : ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Full source

theorem sUnion_eq_compl_sInter_compl (S : Set (Set α)) : ⋃₀ S = (⋂₀ (compl '' S))ᶜ := by
  rw [← compl_compl (⋃₀ S), compl_sUnion]

Union as Complement of Intersection of Complements

Informal description

For any family of sets $S \subseteq \mathcal{P}(\alpha)$, the union $\bigcup_{X \in S} X$ is equal to the complement of the intersection of the complements of all sets in $S$. That is, \[ \bigcup_{X \in S} X = \left( \bigcap_{X \in S} X^c \right)^c. \]

Set.compl_sInter theorem

(S : Set (Set α)) : (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Full source

theorem compl_sInter (S : Set (Set α)) : (⋂₀ S)ᶜ = ⋃₀ (compl '' S) := by
  rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

De Morgan's Law for Set Intersection: Complement of Intersection Equals Union of Complements

Informal description

For any family of sets $S \subseteq \mathcal{P}(\alpha)$, the complement of the intersection $\bigcap_{X \in S} X$ is equal to the union of the complements of all sets in $S$. That is, \[ \left( \bigcap_{X \in S} X \right)^c = \bigcup_{X \in S} X^c. \]

Set.sInter_eq_compl_sUnion_compl theorem

(S : Set (Set α)) : ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Full source

theorem sInter_eq_compl_sUnion_compl (S : Set (Set α)) : ⋂₀ S = (⋃₀ (compl '' S))ᶜ := by
  rw [← compl_compl (⋂₀ S), compl_sInter]

De Morgan's Law for Set Intersection: Intersection Equals Complement of Union of Complements

Informal description

For any family of sets $S \subseteq \mathcal{P}(\alpha)$, the intersection $\bigcap_{X \in S} X$ is equal to the complement of the union of the complements of all sets in $S$. That is, \[ \bigcap_{X \in S} X = \left( \bigcup_{X \in S} X^c \right)^c. \]

Set.inter_empty_of_inter_sUnion_empty theorem

{s t : Set α} {S : Set (Set α)} (hs : t ∈ S) (h : s ∩ ⋃₀ S = ∅) : s ∩ t = ∅

Full source

theorem inter_empty_of_inter_sUnion_empty {s t : Set α} {S : Set (Set α)} (hs : t ∈ S)
    (h : s ∩ ⋃₀ S = ∅) : s ∩ t = ∅ :=
  eq_empty_of_subset_empty <| by
    rw [← h]; exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

Intersection with a Set in a Family is Empty if Intersection with the Union is Empty

Informal description

For any sets $s, t \subseteq \alpha$ and any family of sets $S \subseteq \mathcal{P}(\alpha)$, if $t \in S$ and $s \cap \bigcup S = \emptyset$, then $s \cap t = \emptyset$.

Set.range_sigma_eq_iUnion_range theorem

{γ : α → Type*} (f : Sigma γ → β) : range f = ⋃ a, range fun b => f ⟨a, b⟩

Full source

theorem range_sigma_eq_iUnion_range {γ : α → Type*} (f : Sigma γ → β) :
    range f = ⋃ a, range fun b => f ⟨a, b⟩ :=
  Set.ext <| by simp

Range of Sigma-Type Function as Union of Component Ranges

Informal description

For any family of types $\{\gamma_a\}_{a \in \alpha}$ and any function $f : \Sigma_{a \in \alpha} \gamma_a \to \beta$, the range of $f$ is equal to the union over $a \in \alpha$ of the ranges of the functions $f \langle a, \cdot \rangle : \gamma_a \to \beta$. That is, $$\text{range } f = \bigcup_{a \in \alpha} \text{range } (b \mapsto f \langle a, b \rangle).$$

Set.iUnion_eq_range_sigma theorem

(s : α → Set β) : ⋃ i, s i = range fun a : Σ i, s i => a.2

Full source

theorem iUnion_eq_range_sigma (s : α → Set β) : ⋃ i, s i = range fun a : Σi, s i => a.2 := by
  simp [Set.ext_iff]

Union of Indexed Family as Range of Dependent Pairs

Informal description

For any indexed family of sets $\{s_i\}_{i \in \alpha}$ where $s_i \subseteq \beta$ for each $i \in \alpha$, the union $\bigcup_{i \in \alpha} s_i$ is equal to the range of the function that maps each dependent pair $(i, x) \in \Sigma_{i \in \alpha} s_i$ to its second component $x$. In other words: $$\bigcup_{i \in \alpha} s_i = \{x \in \beta \mid \exists (i \in \alpha, y \in s_i), x = y\}.$$

Set.iUnion_eq_range_psigma theorem

(s : ι → Set β) : ⋃ i, s i = range fun a : Σ' i, s i => a.2

Full source

theorem iUnion_eq_range_psigma (s : ι → Set β) : ⋃ i, s i = range fun a : Σ'i, s i => a.2 := by
  simp [Set.ext_iff]

Union of Indexed Family as Range of Dependent Pairs

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$, the union $\bigcup_{i \in \iota} s_i$ is equal to the range of the function that maps each dependent pair $(i, x) \in \Sigma'_{i \in \iota} s_i$ to its second component $x$.

Set.iUnion_image_preimage_sigma_mk_eq_self theorem

{ι : Type*} {σ : ι → Type*} (s : Set (Sigma σ)) : ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s

Full source

theorem iUnion_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : Set (Sigma σ)) :
    ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s := by
  ext x
  simp only [mem_iUnion, mem_image, mem_preimage]
  constructor
  · rintro ⟨i, a, h, rfl⟩
    exact h
  · intro h
    obtain ⟨i, a⟩ := x
    exact ⟨i, a, h, rfl⟩

Union of Preimage-Image Construction via Dependent Pairs Equals Original Set

Informal description

For any family of types $\{\sigma_i\}_{i \in \iota}$ indexed by $\iota$ and any subset $s$ of the dependent sum type $\Sigma_{i \in \iota} \sigma_i$, the union over all $i \in \iota$ of the images of the preimages of $s$ under the dependent pair constructor $\Sigma.\text{mk}_i$ equals $s$ itself. In other words: \[ \bigcup_{i \in \iota} \Sigma.\text{mk}_i \left( \Sigma.\text{mk}_i^{-1}(s) \right) = s \]

Set.Sigma.univ theorem

(X : α → Type*) : (Set.univ : Set (Σ a, X a)) = ⋃ a, range (Sigma.mk a)

Full source

theorem Sigma.univ (X : α → Type*) : (Set.univ : Set (Σa, X a)) = ⋃ a, range (Sigma.mk a) :=
  Set.ext fun x =>
    iff_of_true trivial ⟨range (Sigma.mk x.1), Set.mem_range_self _, x.2, Sigma.eta x⟩

Universal Set as Union of Dependent Pair Ranges

Informal description

For any family of types $\{X_a\}_{a \in \alpha}$, the universal set of the dependent sum type $\Sigma_{a \in \alpha} X_a$ is equal to the union over all $a \in \alpha$ of the ranges of the dependent pair constructors $\Sigma.\text{mk}_a : X_a \to \Sigma_{a \in \alpha} X_a$. In other words: \[ \text{univ} = \bigcup_{a \in \alpha} \text{range}(\Sigma.\text{mk}_a). \]

Set.iUnion_subset_iUnion_const theorem

{s : Set α} (h : ι → ι₂) : ⋃ _ : ι, s ⊆ ⋃ _ : ι₂, s

Full source

theorem iUnion_subset_iUnion_const {s : Set α} (h : ι → ι₂) : ⋃ _ : ι, s⋃ _ : ι, s ⊆ ⋃ _ : ι₂, s :=
  iSup_const_mono (α := Set α) h

Union Subset Under Index Transformation

Informal description

For any set $s$ in a type $\alpha$ and any function $h$ from an index type $\iota$ to another index type $\iota_2$, the union of $s$ over all elements of $\iota$ is a subset of the union of $s$ over all elements of $\iota_2$. In other words, $\bigcup_{i \in \iota} s \subseteq \bigcup_{j \in \iota_2} s$.

Set.iUnion_singleton_eq_range theorem

(f : α → β) : ⋃ x : α, {f x} = range f

Full source

@[simp]
theorem iUnion_singleton_eq_range (f : α → β) : ⋃ x : α, {f x} = range f := by
  ext x
  simp [@eq_comm _ x]

Union of Singletons Equals Range of Function

Informal description

For any function $f : \alpha \to \beta$, the union of all singleton sets $\{f(x)\}$ over all $x \in \alpha$ is equal to the range of $f$, i.e., \[ \bigcup_{x \in \alpha} \{f(x)\} = \text{range}(f). \]

Set.iUnion_insert_eq_range_union_iUnion theorem

{ι : Type*} (x : ι → β) (t : ι → Set β) : ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i

Full source

theorem iUnion_insert_eq_range_union_iUnion {ι : Type*} (x : ι → β) (t : ι → Set β) :
    ⋃ i, insert (x i) (t i) = rangerange x ∪ ⋃ i, t i := by
  simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]

Union of Insertions Equals Range Union with Indexed Union

Informal description

For any indexed family of elements $x_i$ in $\beta$ and any indexed family of sets $t_i$ in $\beta$, the union over all $i$ of the sets obtained by inserting $x_i$ into $t_i$ equals the union of the range of $x$ with the union of all $t_i$. In symbols: \[ \bigcup_{i} \{x_i\} \cup t_i = \text{range}(x) \cup \bigcup_{i} t_i. \]

Set.iUnion_of_singleton theorem

(α : Type*) : (⋃ x, { x } : Set α) = univ

Full source

theorem iUnion_of_singleton (α : Type*) : (⋃ x, {x} : Set α) = univ := by simp [Set.ext_iff]

Union of Singletons is Universal Set

Informal description

For any type $\alpha$, the union over all $x \in \alpha$ of the singleton sets $\{x\}$ is equal to the universal set $\text{univ}$ of $\alpha$, i.e., $\bigcup_{x \in \alpha} \{x\} = \text{univ}$.

Set.iUnion_of_singleton_coe theorem

(s : Set α) : ⋃ i : s, ({(i : α)} : Set α) = s

Full source

theorem iUnion_of_singleton_coe (s : Set α) : ⋃ i : s, ({(i : α)} : Set α) = s := by simp

Union of Singletons over Subset Equals Subset

Informal description

For any subset $s$ of a type $\alpha$, the union of all singleton sets $\{i\}$ for $i \in s$ is equal to $s$ itself, i.e., \[ \bigcup_{i \in s} \{i\} = s. \]

Set.sUnion_eq_biUnion theorem

{s : Set (Set α)} : ⋃₀ s = ⋃ (i : Set α) (_ : i ∈ s), i

Full source

theorem sUnion_eq_biUnion {s : Set (Set α)} : ⋃₀ s = ⋃ (i : Set α) (_ : i ∈ s), i := by
  rw [← sUnion_image, image_id']

Union of a Family of Sets Equals Bounded Union

Informal description

For any family of sets $s$ (where each element of $s$ is a subset of $\alpha$), the union of all sets in $s$ equals the union of all sets $i$ over $i \in s$. In symbols: \[ \bigcup₀ s = \bigcup_{i \in s} i \]

Set.sInter_eq_biInter theorem

{s : Set (Set α)} : ⋂₀ s = ⋂ (i : Set α) (_ : i ∈ s), i

Full source

theorem sInter_eq_biInter {s : Set (Set α)} : ⋂₀ s = ⋂ (i : Set α) (_ : i ∈ s), i := by
  rw [← sInter_image, image_id']

Intersection of a Family of Sets as Bounded Intersection

Informal description

For any family of sets $s$ in a type $\alpha$, the intersection of all sets in $s$ (denoted $\bigcap₀ s$) is equal to the intersection of all sets $i$ where $i$ ranges over $s$ (denoted $\bigcap_{i \in s} i$).

Set.sUnion_eq_iUnion theorem

{s : Set (Set α)} : ⋃₀ s = ⋃ i : s, i

Full source

theorem sUnion_eq_iUnion {s : Set (Set α)} : ⋃₀ s = ⋃ i : s, i := by
  simp only [← sUnion_range, Subtype.range_coe]

Union of a Family of Sets Equals Indexed Union

Informal description

For any family of sets $s$ in a type $\alpha$, the union of all sets in $s$ (denoted $\bigcup₀ s$) is equal to the union of all sets $i$ where $i$ ranges over $s$ (denoted $\bigcup_{i \in s} i$).

Set.sInter_eq_iInter theorem

{s : Set (Set α)} : ⋂₀ s = ⋂ i : s, i

Full source

theorem sInter_eq_iInter {s : Set (Set α)} : ⋂₀ s = ⋂ i : s, i := by
  simp only [← sInter_range, Subtype.range_coe]

Intersection of a Family of Sets as Indexed Intersection

Informal description

For any family of sets $s$ in a type $\alpha$, the intersection of all sets in $s$ (denoted $\bigcap₀ s$) is equal to the intersection over all sets $i$ in $s$ (denoted $\bigcap_{i \in s} i$).

Set.iUnion_of_empty theorem

[IsEmpty ι] (s : ι → Set α) : ⋃ i, s i = ∅

Full source

@[simp]
theorem iUnion_of_empty [IsEmpty ι] (s : ι → Set α) : ⋃ i, s i = ∅ :=
  iSup_of_empty _

Union of Empty Family is Empty Set

Informal description

For any type `ι` that is empty (i.e., has no elements) and any family of sets `s : ι → Set α`, the union of all sets in the family is the empty set, i.e., $\bigcup_{i} s(i) = \emptyset$.

Set.iInter_of_empty theorem

[IsEmpty ι] (s : ι → Set α) : ⋂ i, s i = univ

Full source

@[simp]
theorem iInter_of_empty [IsEmpty ι] (s : ι → Set α) : ⋂ i, s i = univ :=
  iInf_of_empty _

Intersection over Empty Index Set is Universal Set

Informal description

For any type `ι` that is empty (i.e., `IsEmpty ι` holds) and any family of sets `s : ι → Set α`, the intersection of all sets in the family is equal to the universal set `univ`. In other words, $\bigcap_{i \in \iota} s(i) = \text{univ}$.

Set.union_eq_iUnion theorem

{s₁ s₂ : Set α} : s₁ ∪ s₂ = ⋃ b : Bool, cond b s₁ s₂

Full source

theorem union_eq_iUnion {s₁ s₂ : Set α} : s₁ ∪ s₂ = ⋃ b : Bool, cond b s₁ s₂ :=
  sup_eq_iSup s₁ s₂

Union as Indexed Union over Boolean Condition

Informal description

For any two sets $s_1$ and $s_2$ in a type $\alpha$, their union $s_1 \cup s_2$ is equal to the indexed union $\bigcup_{b \in \text{Bool}} \text{cond}(b, s_1, s_2)$, where $\text{cond}$ is the boolean conditional function that selects $s_1$ when $b$ is true and $s_2$ when $b$ is false.

Set.inter_eq_iInter theorem

{s₁ s₂ : Set α} : s₁ ∩ s₂ = ⋂ b : Bool, cond b s₁ s₂

Full source

theorem inter_eq_iInter {s₁ s₂ : Set α} : s₁ ∩ s₂ = ⋂ b : Bool, cond b s₁ s₂ :=
  inf_eq_iInf s₁ s₂

Intersection as Boolean-indexed Intersection

Informal description

For any two sets $s₁$ and $s₂$ in a type $\alpha$, their intersection $s₁ ∩ s₂$ is equal to the intersection of the family of sets indexed by the boolean type, where the family is defined by $s(b) = \text{cond } b \text{ } s₁ \text{ } s₂$ (i.e., $s(\text{true}) = s₁$ and $s(\text{false}) = s₂$). In other words: $$ s₁ ∩ s₂ = \bigcap_{b \in \text{Bool}} \text{cond } b \text{ } s₁ \text{ } s₂ $$

Set.sInter_union_sInter theorem

{S T : Set (Set α)} : ⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, (p : Set α × Set α).1 ∪ p.2

Full source

theorem sInter_union_sInter {S T : Set (Set α)} :
    ⋂₀ S⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, (p : Set α × Set α).1 ∪ p.2 :=
  sInf_sup_sInf

Union of Intersections Equals Intersection of Pairwise Unions

Informal description

For any two collections of sets $S$ and $T$ in a type $\alpha$, the union of the intersection of all sets in $S$ and the intersection of all sets in $T$ is equal to the intersection over all pairs $(s,t) \in S \times T$ of the unions $s \cup t$. In symbols: \[ \bigcap S \cup \bigcap T = \bigcap_{(s,t) \in S \times T} (s \cup t) \]

Set.sUnion_inter_sUnion theorem

{s t : Set (Set α)} : ⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, (p : Set α × Set α).1 ∩ p.2

Full source

theorem sUnion_inter_sUnion {s t : Set (Set α)} :
    ⋃₀ s⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, (p : Set α × Set α).1 ∩ p.2 :=
  sSup_inf_sSup

Intersection of Unions Equals Union of Pairwise Intersections

Informal description

For any two families of sets $s$ and $t$ in a type $\alpha$, the intersection of their set unions equals the union of pairwise intersections. More precisely: \[ \left( \bigcup_{A \in s} A \right) \cap \left( \bigcup_{B \in t} B \right) = \bigcup_{(A,B) \in s \times t} (A \cap B) \]

Set.biUnion_iUnion theorem

(s : ι → Set α) (t : α → Set β) : ⋃ x ∈ ⋃ i, s i, t x = ⋃ (i) (x ∈ s i), t x

Full source

theorem biUnion_iUnion (s : ι → Set α) (t : α → Set β) :
    ⋃ x ∈ ⋃ i, s i, t x = ⋃ (i) (x ∈ s i), t x := by simp [@iUnion_comm _ ι]

Double Union Equivalence for Bounded Union over Union

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any family of sets $\{t_x\}_{x \in \alpha}$ in a type $\beta$, the union over all $x$ in the union of the $s_i$ of the sets $t_x$ is equal to the double union over all $i \in \iota$ and all $x \in s_i$ of the sets $t_x$. In symbols: \[ \bigcup_{x \in \bigcup_{i} s_i} t_x = \bigcup_{i \in \iota} \bigcup_{x \in s_i} t_x. \]

Set.biInter_iUnion theorem

(s : ι → Set α) (t : α → Set β) : ⋂ x ∈ ⋃ i, s i, t x = ⋂ (i) (x ∈ s i), t x

Full source

theorem biInter_iUnion (s : ι → Set α) (t : α → Set β) :
    ⋂ x ∈ ⋃ i, s i, t x = ⋂ (i) (x ∈ s i), t x := by simp [@iInter_comm _ ι]

Double Intersection over Union Equals Nested Intersection

Informal description

For any family of sets $s : \iota \to \text{Set } \alpha$ and any family of sets $t : \alpha \to \text{Set } \beta$, the intersection of all sets $t(x)$ where $x$ ranges over the union $\bigcup_i s(i)$ is equal to the double intersection over all indices $i$ and all elements $x \in s(i)$ of the sets $t(x)$. That is, \[ \bigcap_{x \in \bigcup_i s(i)} t(x) = \bigcap_i \bigcap_{x \in s(i)} t(x). \]

Set.sUnion_iUnion theorem

(s : ι → Set (Set α)) : ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i

Full source

theorem sUnion_iUnion (s : ι → Set (Set α)) : ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i := by
  simp only [sUnion_eq_biUnion, biUnion_iUnion]

Union of Unions Equals Union of Set Unions

Informal description

For any family of sets of sets $\{s_i\}_{i \in \iota}$ (where each $s_i$ is a collection of subsets of $\alpha$), the union of all sets in the union $\bigcup_i s_i$ equals the union over all indices $i$ of the unions of the sets in $s_i$. In symbols: \[ \bigcup₀ \left(\bigcup_{i} s_i\right) = \bigcup_{i} \left(\bigcup₀ s_i\right). \]

Set.sInter_iUnion theorem

(s : ι → Set (Set α)) : ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i

Full source

theorem sInter_iUnion (s : ι → Set (Set α)) : ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i := by
  simp only [sInter_eq_biInter, biInter_iUnion]

Intersection of Union of Families Equals Nested Intersection

Informal description

For any family of sets of sets $s : \iota \to \text{Set } (\text{Set } \alpha)$, the intersection of all sets in the union $\bigcup_i s(i)$ is equal to the intersection over all indices $i$ of the intersections of the sets in $s(i)$. That is, \[ \bigcap₀ \left(\bigcup_{i} s(i)\right) = \bigcap_{i} \left(\bigcap₀ s(i)\right). \]

Set.iUnion_range_eq_sUnion theorem

 {α β : Type*} (C : Set (Set α)) {f : ∀ s : C, β → (s : Type _)} (hf : ∀ s : C, Surjective (f s)) :
  ⋃ y : β, range (fun s : C => (f s y).val) = ⋃₀ C

Full source

theorem iUnion_range_eq_sUnion {α β : Type*} (C : Set (Set α)) {f : ∀ s : C, β → (s : Type _)}
    (hf : ∀ s : C, Surjective (f s)) : ⋃ y : β, range (fun s : C => (f s y).val) = ⋃₀ C := by
  ext x; constructor
  · rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
    refine ⟨_, hs, ?_⟩
    exact (f ⟨s, hs⟩ y).2
  · rintro ⟨s, hs, hx⟩
    obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩
    refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩
    exact congr_arg Subtype.val hy

Union of Ranges Equals Union of Collection under Surjective Indexing

Informal description

Let $C$ be a collection of subsets of a type $\alpha$, and for each $s \in C$, let $f_s : \beta \to s$ be a surjective function. Then the union over all $y \in \beta$ of the ranges of the functions $\lambda s \in C, (f_s y).val$ is equal to the union of all sets in $C$. In symbols: $$ \bigcup_{y \in \beta} \text{range}\left(\lambda s \in C, (f_s y).val\right) = \bigcup_{s \in C} s. $$

Set.iUnion_range_eq_iUnion theorem

 (C : ι → Set α) {f : ∀ x : ι, β → C x} (hf : ∀ x : ι, Surjective (f x)) :
  ⋃ y : β, range (fun x : ι => (f x y).val) = ⋃ x, C x

Full source

theorem iUnion_range_eq_iUnion (C : ι → Set α) {f : ∀ x : ι, β → C x}
    (hf : ∀ x : ι, Surjective (f x)) : ⋃ y : β, range (fun x : ι => (f x y).val) = ⋃ x, C x := by
  ext x; rw [mem_iUnion, mem_iUnion]; constructor
  · rintro ⟨y, i, rfl⟩
    exact ⟨i, (f i y).2⟩
  · rintro ⟨i, hx⟩
    obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
    exact ⟨y, i, congr_arg Subtype.val hy⟩

Union of Ranges of Surjective Family Equals Union of Family

Informal description

Let $\{C_i\}_{i \in \iota}$ be a family of sets in $\alpha$, and for each $i \in \iota$, let $f_i : \beta \to C_i$ be a surjective function. Then the union over $y \in \beta$ of the ranges of the functions $\lambda x \mapsto (f_x y).\text{val}$ equals the union of the family $\{C_i\}_{i \in \iota}$. In symbols: $$ \bigcup_{y \in \beta} \text{range}\left(\lambda x \mapsto (f_x y).\text{val}\right) = \bigcup_{x \in \iota} C_x $$

Set.union_distrib_iInter_left theorem

(s : ι → Set α) (t : Set α) : (t ∪ ⋂ i, s i) = ⋂ i, t ∪ s i

Full source

theorem union_distrib_iInter_left (s : ι → Set α) (t : Set α) : (t ∪ ⋂ i, s i) = ⋂ i, t ∪ s i :=
  sup_iInf_eq _ _

Distributivity of Union over Intersection (Left Version)

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the union of $t$ with the intersection of all $s_i$ equals the intersection of all unions $t \cup s_i$. In symbols: $$ t \cup \left( \bigcap_{i} s_i \right) = \bigcap_{i} (t \cup s_i) $$

Set.union_distrib_iInter₂_left theorem

(s : Set α) (t : ∀ i, κ i → Set α) : (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j

Full source

theorem union_distrib_iInter₂_left (s : Set α) (t : ∀ i, κ i → Set α) :
    (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j := by simp_rw [union_distrib_iInter_left]

Double Distributivity of Union over Intersection (Left Version)

Informal description

For any set $s$ in a type $\alpha$ and any doubly-indexed family of sets $\{t_{i,j}\}_{i \in \kappa, j \in \kappa_i}$ in $\alpha$, the union of $s$ with the double intersection of all $t_{i,j}$ equals the double intersection of all unions $s \cup t_{i,j}$. In symbols: $$ s \cup \left( \bigcap_{i,j} t_{i,j} \right) = \bigcap_{i,j} (s \cup t_{i,j}) $$

Set.union_distrib_iInter_right theorem

(s : ι → Set α) (t : Set α) : (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t

Full source

theorem union_distrib_iInter_right (s : ι → Set α) (t : Set α) : (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t :=
  iInf_sup_eq _ _

Distributivity of Union over Intersection (Right)

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the union of the intersection $\bigcap_i s_i$ with $t$ equals the intersection of the unions $s_i \cup t$ for all $i \in \iota$. That is, \[ \left(\bigcap_{i \in \iota} s_i\right) \cup t = \bigcap_{i \in \iota} (s_i \cup t). \]

Set.union_distrib_iInter₂_right theorem

(s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t

Full source

theorem union_distrib_iInter₂_right (s : ∀ i, κ i → Set α) (t : Set α) :
    (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t := by simp_rw [union_distrib_iInter_right]

Distributivity of Union over Doubly-Indexed Intersection (Right)

Informal description

For any doubly-indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the union of the intersection $\bigcap_{i,j} s_{i,j}$ with $t$ equals the intersection of the unions $s_{i,j} \cup t$ for all $i \in \iota$ and $j \in \kappa_i$. That is, \[ \left(\bigcap_{i \in \iota} \bigcap_{j \in \kappa_i} s_{i,j}\right) \cup t = \bigcap_{i \in \iota} \bigcap_{j \in \kappa_i} (s_{i,j} \cup t). \]

Set.biUnion_lt_eq_iUnion theorem

[LT α] [NoMaxOrder α] {s : α → Set β} : ⋃ (n) (m < n), s m = ⋃ n, s n

Full source

lemma biUnion_lt_eq_iUnion [LT α] [NoMaxOrder α] {s : α → Set β} :
    ⋃ (n) (m < n), s m = ⋃ n, s n := biSup_lt_eq_iSup

Union of Predecessor Sets Equals Full Union in No-Max-Order Types

Informal description

Let $\alpha$ be a type with a strict order relation $<$ and no maximal element, and let $\beta$ be another type. For any family of sets $(s_n)_{n \in \alpha}$ in $\beta$, the union $\bigcup_{n \in \alpha} \bigcup_{m < n} s_m$ equals $\bigcup_{n \in \alpha} s_n$.

Set.biUnion_le_eq_iUnion theorem

[Preorder α] {s : α → Set β} : ⋃ (n) (m ≤ n), s m = ⋃ n, s n

Full source

lemma biUnion_le_eq_iUnion [Preorder α] {s : α → Set β} :
    ⋃ (n) (m ≤ n), s m = ⋃ n, s n := biSup_le_eq_iSup

Union of Bounded Unions Equals Union of All Sets in Preorder

Informal description

For any preorder $\alpha$ and any family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the union of all sets $s_m$ where $m \leq n$ for some $n \in \alpha$ is equal to the union of all sets $s_n$ over $n \in \alpha$. In symbols: \[ \bigcup_{n \in \alpha} \bigcup_{m \leq n} s_m = \bigcup_{n \in \alpha} s_n \]

Set.biInter_lt_eq_iInter theorem

[LT α] [NoMaxOrder α] {s : α → Set β} : ⋂ (n) (m < n), s m = ⋂ (n), s n

Full source

lemma biInter_lt_eq_iInter [LT α] [NoMaxOrder α] {s : α → Set β} :
    ⋂ (n) (m < n), s m = ⋂ (n), s n := biInf_lt_eq_iInf

Intersection of Sets Indexed by Lesser Elements Equals Intersection of All Sets

Informal description

Let $\alpha$ be a type equipped with a strict order $<$ and no maximal element, and let $\beta$ be another type. For any family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the intersection of all sets $s_m$ where $m < n$ for some $n \in \alpha$ equals the intersection of all sets $s_n$ over $n \in \alpha$. In symbols: \[ \bigcap_{n \in \alpha} \bigcap_{m < n} s_m = \bigcap_{n \in \alpha} s_n. \]

Set.biInter_le_eq_iInter theorem

[Preorder α] {s : α → Set β} : ⋂ (n) (m ≤ n), s m = ⋂ (n), s n

Full source

lemma biInter_le_eq_iInter [Preorder α] {s : α → Set β} :
    ⋂ (n) (m ≤ n), s m = ⋂ (n), s n := biInf_le_eq_iInf

Intersection of Sets Indexed by Less-Or-Equal Elements Equals Intersection of All Sets

Informal description

Let $\alpha$ be a type with a preorder $\leq$, and let $\beta$ be another type. For any family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the intersection of all sets $s_m$ where $m \leq n$ for some $n \in \alpha$ equals the intersection of all sets $s_n$ over $n \in \alpha$. In symbols: \[ \bigcap_{n \in \alpha} \bigcap_{m \leq n} s_m = \bigcap_{n \in \alpha} s_n. \]

Set.biUnion_gt_eq_iUnion theorem

[LT α] [NoMinOrder α] {s : α → Set β} : ⋃ (n) (m > n), s m = ⋃ n, s n

Full source

lemma biUnion_gt_eq_iUnion [LT α] [NoMinOrder α] {s : α → Set β} :
    ⋃ (n) (m > n), s m = ⋃ n, s n := biSup_gt_eq_iSup

Union of Sets Indexed by Greater Elements Equals Union of All Sets

Informal description

Let $\alpha$ be a type with a strict order $<$ and no minimal element, and let $\beta$ be another type. For any family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the union of all sets $s_m$ where $m > n$ for some $n \in \alpha$ equals the union of all sets $s_n$ over $n \in \alpha$. In symbols: \[ \bigcup_{n \in \alpha} \bigcup_{m > n} s_m = \bigcup_{n \in \alpha} s_n. \]

Set.biUnion_ge_eq_iUnion theorem

[Preorder α] {s : α → Set β} : ⋃ (n) (m ≥ n), s m = ⋃ n, s n

Full source

lemma biUnion_ge_eq_iUnion [Preorder α] {s : α → Set β} :
    ⋃ (n) (m ≥ n), s m = ⋃ n, s n := biSup_ge_eq_iSup

Union of Sets Indexed by Greater or Equal Elements Equals Union of All Sets

Informal description

Let $\alpha$ be a type with a preorder $\leq$ and $\beta$ be another type. For any family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the union of all sets $s_m$ where $m \geq n$ for some $n \in \alpha$ equals the union of all sets $s_n$ over $n \in \alpha$. In symbols: \[ \bigcup_{n \in \alpha} \bigcup_{m \geq n} s_m = \bigcup_{n \in \alpha} s_n. \]

Set.biInter_gt_eq_iInf theorem

[LT α] [NoMinOrder α] {s : α → Set β} : ⋂ (n) (m > n), s m = ⋂ n, s n

Full source

lemma biInter_gt_eq_iInf [LT α] [NoMinOrder α] {s : α → Set β} :
    ⋂ (n) (m > n), s m = ⋂ n, s n := biInf_gt_eq_iInf

Intersection of Sets Indexed by Greater Elements Equals Intersection of All Sets

Informal description

Let $\alpha$ be a type with a strict order $<$ and no minimal element, and let $\beta$ be another type. For any family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the intersection of all sets $s_m$ where $m > n$ for some $n \in \alpha$ equals the intersection of all sets $s_n$ over $n \in \alpha$. In symbols: \[ \bigcap_{n \in \alpha} \bigcap_{m > n} s_m = \bigcap_{n \in \alpha} s_n. \]

Set.biInter_ge_eq_iInf theorem

[Preorder α] {s : α → Set β} : ⋂ (n) (m ≥ n), s m = ⋂ n, s n

Full source

lemma biInter_ge_eq_iInf [Preorder α] {s : α → Set β} :
    ⋂ (n) (m ≥ n), s m = ⋂ n, s n := biInf_ge_eq_iInf

Intersection of Tail Sets Equals Overall Intersection

Informal description

Let $\alpha$ be a preorder and $\beta$ be any type. Given a family of sets $\{s_n\}_{n \in \alpha}$ indexed by $\alpha$, the intersection of all sets $s_m$ where $m \geq n$ (for each $n$) equals the intersection of all sets $s_n$. In symbols: \[ \bigcap_{n \in \alpha} \bigcap_{m \geq n} s_m = \bigcap_{n \in \alpha} s_n. \]

Set.biUnion_le theorem

: (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i

Full source

theorem biUnion_le : (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i :=
  biSup_le_eq_sup s i

Union of Sets Up to Index Equals Union of Strictly Smaller Sets Plus Current Set

Informal description

For any indexed family of sets $\{s_j\}$ and any index $i$, the union of all sets $s_j$ with $j \leq i$ equals the union of all sets $s_j$ with $j < i$ together with the set $s_i$. In symbols: \[ \bigcup_{j \leq i} s_j = \left(\bigcup_{j < i} s_j\right) \cup s_i. \]

Set.biInter_le theorem

: (⋂ j ≤ i, s j) = (⋂ j < i, s j) ∩ s i

Full source

theorem biInter_le : (⋂ j ≤ i, s j) = (⋂ j < i, s j) ∩ s i :=
  biInf_le_eq_inf s i

Intersection of Sets Up to $i$ Equals Intersection Before $i$ Intersected with $s_i$

Informal description

For any family of sets $\{s_j\}_{j \in \alpha}$ indexed by a preorder $\alpha$ and any element $i \in \alpha$, the intersection of all sets $s_j$ with $j \leq i$ is equal to the intersection of all sets $s_j$ with $j < i$ intersected with $s_i$. In symbols: \[ \bigcap_{j \leq i} s_j = \left(\bigcap_{j < i} s_j\right) \cap s_i. \]

Set.biUnion_ge theorem

: (⋃ j ≥ i, s j) = s i ∪ ⋃ j > i, s j

Full source

theorem biUnion_ge : (⋃ j ≥ i, s j) = s i ∪ ⋃ j > i, s j :=
  biSup_ge_eq_sup s i

Union of Sets Indexed by Greater or Equal Condition

Informal description

For an indexed family of sets $s_j$, the union of all sets $s_j$ with $j \geq i$ is equal to the union of $s_i$ with the union of all sets $s_j$ where $j > i$. In symbols: \[ \bigcup_{j \geq i} s_j = s_i \cup \bigcup_{j > i} s_j \]

Set.biInter_ge theorem

: (⋂ j ≥ i, s j) = s i ∩ ⋂ j > i, s j

Full source

theorem biInter_ge : (⋂ j ≥ i, s j) = s i ∩ ⋂ j > i, s j :=
  biInf_ge_eq_inf s i

Intersection Decomposition for Indexed Family of Sets

Informal description

For any index $i$ and any family of sets $\{s_j\}$, the intersection of all sets $s_j$ with $j \geq i$ is equal to the intersection of $s_i$ with the intersection of all sets $s_j$ where $j > i$. In symbols: \[ \bigcap_{j \geq i} s_j = s_i \cap \bigcap_{j > i} s_j \]

Set.pi_def theorem

(i : Set α) (s : ∀ a, Set (π a)) : pi i s = ⋂ a ∈ i, eval a ⁻¹' s a

Full source

theorem pi_def (i : Set α) (s : ∀ a, Set (π a)) : pi i s = ⋂ a ∈ i, eval a ⁻¹' s a := by
  ext
  simp

Product Set as Intersection of Preimages

Informal description

For any set $i \subseteq \alpha$ and any family of sets $\{s_a\}_{a \in \alpha}$, the product set $\prod_{a \in i} s_a$ is equal to the intersection over all $a \in i$ of the preimages of $s_a$ under the evaluation function at $a$. In symbols: \[ \prod_{a \in i} s_a = \bigcap_{a \in i} \text{eval}_a^{-1}(s_a) \]

Set.univ_pi_eq_iInter theorem

(t : ∀ i, Set (π i)) : pi univ t = ⋂ i, eval i ⁻¹' t i

Full source

theorem univ_pi_eq_iInter (t : ∀ i, Set (π i)) : pi univ t = ⋂ i, eval i ⁻¹' t i := by
  simp only [pi_def, iInter_true, mem_univ]

Universal Product Set as Intersection of Preimages

Informal description

For any family of sets $\{t_i\}_{i \in \alpha}$, the product set $\prod_{i \in \alpha} t_i$ is equal to the intersection over all $i \in \alpha$ of the preimages of $t_i$ under the evaluation function at $i$. In symbols: \[ \prod_{i \in \alpha} t_i = \bigcap_{i \in \alpha} \text{eval}_i^{-1}(t_i) \]

Set.pi_diff_pi_subset theorem

(i : Set α) (s t : ∀ a, Set (π a)) : pi i s \ pi i t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)

Full source

theorem pi_diff_pi_subset (i : Set α) (s t : ∀ a, Set (π a)) :
    pipi i s \ pi i tpi i s \ pi i t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a) := by
  refine diff_subset_comm.2 fun x hx a ha => ?_
  simp only [mem_diff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not,
    eval_apply] at hx
  exact hx.2 _ ha (hx.1 _ ha)

Difference of Product Sets is Contained in Union of Preimages of Differences

Informal description

For any index set $i \subseteq \alpha$ and families of sets $s, t : \forall a, \text{Set } (\pi a)$, the difference of the product sets $\prod_{a \in i} s(a) \setminus \prod_{a \in i} t(a)$ is contained in the union over $a \in i$ of the preimages under evaluation of the set differences $s(a) \setminus t(a)$. In symbols: \[ \left(\prod_{a \in i} s(a)\right) \setminus \left(\prod_{a \in i} t(a)\right) \subseteq \bigcup_{a \in i} \text{eval}_a^{-1}(s(a) \setminus t(a)) \]

Set.iUnion_univ_pi theorem

 {ι : α → Type*} (t : (a : α) → ι a → Set (π a)) :
  ⋃ x : (a : α) → ι a, pi univ (fun a => t a (x a)) = pi univ fun a => ⋃ j : ι a, t a j

Full source

theorem iUnion_univ_pi {ι : α → Type*} (t : (a : α) → ι a → Set (π a)) :
    ⋃ x : (a : α) → ι a, pi univ (fun a => t a (x a)) = pi univ fun a => ⋃ j : ι a, t a j := by
  ext
  simp [Classical.skolem]

Union of Product Sets Equals Product of Unions

Informal description

Let $\{ \iota_a \}_{a \in \alpha}$ be a family of types indexed by $\alpha$, and for each $a \in \alpha$, let $\{ t_a(j) \}_{j \in \iota_a}$ be a family of sets in $\pi_a$. Then the union over all functions $x : \prod_{a \in \alpha} \iota_a$ of the product set $\prod_{a \in \alpha} t_a(x(a))$ equals the product set $\prod_{a \in \alpha} \bigcup_{j \in \iota_a} t_a(j)$. In symbols: \[ \bigcup_{x : \prod_{a \in \alpha} \iota_a} \prod_{a \in \alpha} t_a(x(a)) = \prod_{a \in \alpha} \bigcup_{j \in \iota_a} t_a(j) \]

Set.directedOn_iUnion theorem

{r} {f : ι → Set α} (hd : Directed (· ⊆ ·) f) (h : ∀ x, DirectedOn r (f x)) : DirectedOn r (⋃ x, f x)

Full source

theorem directedOn_iUnion {r} {f : ι → Set α} (hd : Directed (· ⊆ ·) f)
    (h : ∀ x, DirectedOn r (f x)) : DirectedOn r (⋃ x, f x) := by
  simp only [DirectedOn, exists_prop, mem_iUnion, exists_imp]
  exact fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
    let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
    let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
    ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩

Directedness of Union under Directed Family of Directed Sets

Informal description

Let $r$ be a relation on a type $\alpha$, and let $f : \iota \to \text{Set } \alpha$ be a family of sets indexed by $\iota$. If $f$ is directed with respect to the subset relation $\subseteq$, and for every $x \in \iota$, the set $f(x)$ is directed with respect to $r$, then the union $\bigcup_{x} f(x)$ is directed with respect to $r$.

Set.directedOn_sUnion theorem

{r} {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S) (h : ∀ x ∈ S, DirectedOn r x) : DirectedOn r (⋃₀ S)

Full source

theorem directedOn_sUnion {r} {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S)
    (h : ∀ x ∈ S, DirectedOn r x) : DirectedOn r (⋃₀ S) := by
  rw [sUnion_eq_iUnion]
  exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

Directedness of Union over Directed Family of Directed Sets

Informal description

Let $r$ be a relation on a type $\alpha$, and let $S$ be a set of subsets of $\alpha$ that is directed with respect to the subset relation $\subseteq$. If for every subset $x \in S$, the set $x$ is directed with respect to $r$, then the union $\bigcup₀ S$ is directed with respect to $r$.

Set.pairwise_iUnion₂ theorem

 {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S) (r : α → α → Prop) (h : ∀ s ∈ S, s.Pairwise r) : (⋃ s ∈ S, s).Pairwise r

Full source

theorem pairwise_iUnion₂ {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S)
    (r : α → α → Prop) (h : ∀ s ∈ S, s.Pairwise r) : (⋃ s ∈ S, s).Pairwise r := by
  simp only [Set.Pairwise, Set.mem_iUnion, exists_prop, forall_exists_index, and_imp]
  intro x S hS hx y T hT hy hne
  obtain ⟨U, hU, hSU, hTU⟩ := hd S hS T hT
  exact h U hU (hSU hx) (hTU hy) hne

Pairwise Relation Preserved Under Directed Union of Sets

Informal description

Let $S$ be a set of subsets of a type $\alpha$ that is directed with respect to the subset relation $\subseteq$, and let $r$ be a binary relation on $\alpha$. If for every subset $s \in S$, the elements of $s$ are pairwise related by $r$, then the elements of the union $\bigcup_{s \in S} s$ are also pairwise related by $r$.

Function.Surjective.iUnion_comp theorem

{f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋃ x, g (f x) = ⋃ y, g y

Full source

theorem iUnion_comp {f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋃ x, g (f x) = ⋃ y, g y :=
  hf.iSup_comp g

Surjective Function Preserves Union: $\bigcup_{x} g(f(x)) = \bigcup_{y} g(y)$

Informal description

Let $f : \iota \to \iota_2$ be a surjective function and $g : \iota_2 \to \mathcal{P}(\alpha)$ be a function mapping to subsets of $\alpha$. Then the union over all $x \in \iota$ of $g(f(x))$ equals the union over all $y \in \iota_2$ of $g(y)$, i.e., \[ \bigcup_{x} g(f(x)) = \bigcup_{y} g(y). \]

Function.Surjective.iInter_comp theorem

{f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋂ x, g (f x) = ⋂ y, g y

Full source

theorem iInter_comp {f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋂ x, g (f x) = ⋂ y, g y :=
  hf.iInf_comp g

Intersection Preservation Under Surjective Precomposition

Informal description

For any surjective function $f \colon \iota \to \iota_2$ and any family of sets $g \colon \iota_2 \to \text{Set } \alpha$, the intersection $\bigcap_{x} g(f(x))$ is equal to $\bigcap_{y} g(y)$.

Set.disjoint_iUnion_left theorem

{ι : Sort*} {s : ι → Set α} : Disjoint (⋃ i, s i) t ↔ ∀ i, Disjoint (s i) t

Full source

@[simp]
theorem disjoint_iUnion_left {ι : Sort*} {s : ι → Set α} :
    DisjointDisjoint (⋃ i, s i) t ↔ ∀ i, Disjoint (s i) t :=
  iSup_disjoint_iff

Disjointness of Union with a Set is Equivalent to Pairwise Disjointness

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the union $\bigcup_{i} s_i$ is disjoint from $t$ if and only if each $s_i$ is disjoint from $t$. In other words: \[ \left(\bigcup_{i} s_i\right) \cap t = \emptyset \quad \text{if and only if} \quad s_i \cap t = \emptyset \text{ for all } i. \]

Set.disjoint_iUnion_right theorem

{ι : Sort*} {s : ι → Set α} : Disjoint t (⋃ i, s i) ↔ ∀ i, Disjoint t (s i)

Full source

@[simp]
theorem disjoint_iUnion_right {ι : Sort*} {s : ι → Set α} :
    DisjointDisjoint t (⋃ i, s i) ↔ ∀ i, Disjoint t (s i) :=
  disjoint_iSup_iff

Disjointness of a Set with a Union is Equivalent to Disjointness with Each Member

Informal description

For any set $t$ and any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, the set $t$ is disjoint from the union $\bigcup_{i} s_i$ if and only if $t$ is disjoint from each individual set $s_i$ in the family.

Set.disjoint_iUnion₂_left theorem

{s : ∀ i, κ i → Set α} {t : Set α} : Disjoint (⋃ (i) (j), s i j) t ↔ ∀ i j, Disjoint (s i j) t

Full source

theorem disjoint_iUnion₂_left {s : ∀ i, κ i → Set α} {t : Set α} :
    DisjointDisjoint (⋃ (i) (j), s i j) t ↔ ∀ i j, Disjoint (s i j) t :=
  iSup₂_disjoint_iff

Disjointness of Double Union with a Set is Equivalent to Pairwise Disjointness

Informal description

For any family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a type $\alpha$ and any set $t \subseteq \alpha$, the union $\bigcup_{i,j} s_{i,j}$ is disjoint from $t$ if and only if each $s_{i,j}$ is disjoint from $t$. In other words: \[ \left(\bigcup_{i,j} s_{i,j}\right) \cap t = \emptyset \quad \text{if and only if} \quad s_{i,j} \cap t = \emptyset \text{ for all } i,j. \]

Set.disjoint_iUnion₂_right theorem

{s : Set α} {t : ∀ i, κ i → Set α} : Disjoint s (⋃ (i) (j), t i j) ↔ ∀ i j, Disjoint s (t i j)

Full source

theorem disjoint_iUnion₂_right {s : Set α} {t : ∀ i, κ i → Set α} :
    DisjointDisjoint s (⋃ (i) (j), t i j) ↔ ∀ i j, Disjoint s (t i j) :=
  disjoint_iSup₂_iff

Disjointness of a Set with a Double Union is Equivalent to Disjointness with Each Member

Informal description

For any set $s$ in a type $\alpha$ and any family of sets $t_i(j)$ indexed by $i$ and $j$, the set $s$ is disjoint from the union $\bigcup_{i,j} t_i(j)$ if and only if $s$ is disjoint from each individual set $t_i(j)$ in the family.

Set.disjoint_sUnion_left theorem

{S : Set (Set α)} {t : Set α} : Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t

Full source

@[simp]
theorem disjoint_sUnion_left {S : Set (Set α)} {t : Set α} :
    DisjointDisjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t :=
  sSup_disjoint_iff

Disjointness of Union of Collection with a Set is Equivalent to Pairwise Disjointness

Informal description

For a collection of sets $S$ in a type $\alpha$ and a set $t \subseteq \alpha$, the union $\bigcup_{s \in S} s$ is disjoint from $t$ if and only if every set $s \in S$ is disjoint from $t$. In other words: \[ \left(\bigcup_{s \in S} s\right) \cap t = \emptyset \quad \text{if and only if} \quad s \cap t = \emptyset \text{ for all } s \in S. \]

Set.disjoint_sUnion_right theorem

{s : Set α} {S : Set (Set α)} : Disjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t

Full source

@[simp]
theorem disjoint_sUnion_right {s : Set α} {S : Set (Set α)} :
    DisjointDisjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t :=
  disjoint_sSup_iff

Disjointness with Union of Collection iff Disjoint with Each Member

Informal description

For any set $s$ and any collection of sets $S$ in a type $\alpha$, the set $s$ is disjoint from the union $\bigcup_{t \in S} t$ if and only if $s$ is disjoint from every set $t$ in $S$.

Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ theorem

 {ι : Type*} {Es : ι → Set α} (Es_union : ⋃ i, Es i = univ) (Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j))
  (I : Set ι) : (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i

Full source

lemma biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ {ι : Type*} {Es : ι → Set α}
    (Es_union : ⋃ i, Es i = univ) (Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j))
    (I : Set ι) :
    (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i := by
  ext x
  obtain ⟨i, hix⟩ : ∃ i, x ∈ Es i := by simp [← mem_iUnion, Es_union]
  have obs : ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es jx ∈ ⋃ j ∈ J, Es j ↔ i ∈ J := by
    refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩
    intro x_in_U
    simp only [mem_iUnion, exists_prop] at x_in_U
    obtain ⟨j, j_in_J, hjx⟩ := x_in_U
    rwa [show i = j by by_contra i_ne_j; exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl]
  have obs' : ∀ (J : Set ι), x ∈ (⋃ j ∈ J, Es j)ᶜx ∈ (⋃ j ∈ J, Es j)ᶜ ↔ i ∉ J :=
    fun J ↦ by simpa only [mem_compl_iff, not_iff_not] using obs J
  rw [obs, obs', mem_compl_iff]

Complement of Union Equals Union of Complements for Partition

Informal description

Let $\{E_i\}_{i \in \iota}$ be a family of pairwise disjoint subsets of $\alpha$ whose union is the entire space (i.e., $\bigcup_{i \in \iota} E_i = \alpha$). Then for any subset $I \subseteq \iota$, the complement of $\bigcup_{i \in I} E_i$ equals $\bigcup_{i \in \iota \setminus I} E_i$. In other words: \[ \left( \bigcup_{i \in I} E_i \right)^c = \bigcup_{i \notin I} E_i. \]

Set.nonempty_iInter_Iic_iff theorem

[Preorder α] {f : ι → α} : (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Full source

lemma nonempty_iInter_Iic_iff [Preorder α] {f : ι → α} :
    (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f) := by
  have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
    ext c; simp [lowerBounds]
  simp [this, BddBelow]

Nonempty Intersection of Left-Infinite Right-Closed Intervals iff Bounded Below

Informal description

For a family of functions $f : \iota \to \alpha$ where $\alpha$ is a preorder, the intersection $\bigcap_i (-\infty, f(i)]$ is nonempty if and only if the range of $f$ is bounded below.

Set.nonempty_iInter_Ici_iff theorem

[Preorder α] {f : ι → α} : (⋂ i, Ici (f i)).Nonempty ↔ BddAbove (range f)

Full source

lemma nonempty_iInter_Ici_iff [Preorder α] {f : ι → α} :
    (⋂ i, Ici (f i)).Nonempty ↔ BddAbove (range f) :=
  nonempty_iInter_Iic_iff (α := αᵒᵈ)

Nonempty Intersection of Right-Infinite Left-Closed Intervals iff Bounded Above

Informal description

For a family of elements $(f_i)_{i \in \iota}$ in a preorder $\alpha$, the intersection $\bigcap_i [f_i, \infty)$ is nonempty if and only if the range of $f$ is bounded above.

Set.Ici_iSup theorem

(f : ι → α) : Ici (⨆ i, f i) = ⋂ i, Ici (f i)

Full source

theorem Ici_iSup (f : ι → α) : Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
  ext fun _ => by simp only [mem_Ici, iSup_le_iff, mem_iInter]

Interval Equality: $[\bigvee_i f_i, \infty) = \bigcap_i [f_i, \infty)$

Informal description

For a family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$, the left-closed right-infinite interval $[\bigvee_i f_i, \infty)$ is equal to the intersection $\bigcap_i [f_i, \infty)$ of all such intervals for each $f_i$.

Set.Iic_iInf theorem

(f : ι → α) : Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Full source

theorem Iic_iInf (f : ι → α) : Iic (⨅ i, f i) = ⋂ i, Iic (f i) :=
  ext fun _ => by simp only [mem_Iic, le_iInf_iff, mem_iInter]

Infimum Interval Equals Intersection of Intervals

Informal description

For any family of elements $(f_i)_{i \in \iota}$ in a complete lattice $\alpha$, the left-infinite right-closed interval $(-\infty, \inf_i f_i]$ is equal to the intersection of the intervals $(-\infty, f_i]$ for all $i \in \iota$. In other words: $$ (-\infty, \inf_i f_i] = \bigcap_{i \in \iota} (-\infty, f_i] $$

Set.Ici_iSup₂ theorem

(f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⋂ (i) (j), Ici (f i j)

Full source

theorem Ici_iSup₂ (f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⋂ (i) (j), Ici (f i j) := by
  simp_rw [Ici_iSup]

Interval Equality for Doubly-Indexed Supremum: $[\bigvee_{i,j} f_{i,j}, \infty) = \bigcap_{i,j} [f_{i,j}, \infty)$

Informal description

For a doubly-indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in a complete lattice $\alpha$, the left-closed right-infinite interval $[\bigvee_{i,j} f_{i,j}, \infty)$ is equal to the intersection $\bigcap_{i,j} [f_{i,j}, \infty)$ of all such intervals for each $f_{i,j}$. In other words: $$ \left[\sup_{i,j} f_{i,j}, \infty\right) = \bigcap_{i,j} [f_{i,j}, \infty) $$

Set.Iic_iInf₂ theorem

(f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⋂ (i) (j), Iic (f i j)

Full source

theorem Iic_iInf₂ (f : ∀ i, κ i → α) : Iic (⨅ (i) (j), f i j) = ⋂ (i) (j), Iic (f i j) := by
  simp_rw [Iic_iInf]

Infimum Interval Equals Intersection of Intervals for Doubly-Indexed Family

Informal description

For any doubly-indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in a complete lattice $\alpha$, the left-infinite right-closed interval $(-\infty, \inf_{i,j} f_{i,j}]$ is equal to the intersection of the intervals $(-\infty, f_{i,j}]$ for all $i \in \iota$ and $j \in \kappa_i$. In other words: $$ (-\infty, \inf_{i,j} f_{i,j}] = \bigcap_{i,j} (-\infty, f_{i,j}] $$

Set.Ici_sSup theorem

(s : Set α) : Ici (sSup s) = ⋂ a ∈ s, Ici a

Full source

theorem Ici_sSup (s : Set α) : Ici (sSup s) = ⋂ a ∈ s, Ici a := by rw [sSup_eq_iSup, Ici_iSup₂]

Supremum Interval Characterization via Intersection of Intervals

Informal description

For any subset $s$ of a complete lattice $\alpha$, the left-closed right-infinite interval $[\sup s, \infty)$ is equal to the intersection $\bigcap_{a \in s} [a, \infty)$ of all such intervals for each element $a \in s$. In other words: $$ [\sup s, \infty) = \bigcap_{a \in s} [a, \infty) $$

Set.Iic_sInf theorem

(s : Set α) : Iic (sInf s) = ⋂ a ∈ s, Iic a

Full source

theorem Iic_sInf (s : Set α) : Iic (sInf s) = ⋂ a ∈ s, Iic a := by rw [sInf_eq_iInf, Iic_iInf₂]

Infimum Interval Characterization via Intersection of Intervals

Informal description

For any subset $s$ of a complete lattice $\alpha$, the left-infinite right-closed interval $(-\infty, \inf s]$ is equal to the intersection of the intervals $(-\infty, a]$ for all $a \in s$. In other words: $$ (-\infty, \inf s] = \bigcap_{a \in s} (-\infty, a] $$

Set.biUnion_diff_biUnion_subset theorem

(s₁ s₂ : Set α) : ((⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x) ⊆ ⋃ x ∈ s₁ \ s₂, t x

Full source

theorem biUnion_diff_biUnion_subset (s₁ s₂ : Set α) :
    ((⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x) ⊆ ⋃ x ∈ s₁ \ s₂, t x := by
  simp only [diff_subset_iff, ← biUnion_union]
  apply biUnion_subset_biUnion_left
  rw [union_diff_self]
  apply subset_union_right

Difference of Bounded Unions is Contained in Bounded Union of Differences

Informal description

For any sets $s_1$ and $s_2$ in a type $\alpha$ and any family of sets $t : \alpha \to \text{Set} \beta$, the difference of the bounded unions satisfies: \[ \left( \bigcup_{x \in s_1} t(x) \right) \setminus \left( \bigcup_{x \in s_2} t(x) \right) \subseteq \bigcup_{x \in s_1 \setminus s_2} t(x) \]

Set.sigmaToiUnion definition

(x : Σ i, t i) : ⋃ i, t i

Full source

/-- If `t` is an indexed family of sets, then there is a natural map from `Σ i, t i` to `⋃ i, t i`
sending `⟨i, x⟩` to `x`. -/
def sigmaToiUnion (x : Σi, t i) : ⋃ i, t i :=
  ⟨x.2, mem_iUnion.2 ⟨x.1, x.2.2⟩⟩

Natural map from dependent sum to union of sets

Informal description

Given an indexed family of sets $ t_i $ (for $ i $ in some index set), there is a natural map from the dependent sum type $ \Sigma i, t_i $ to the union $ \bigcup_i t_i $, which sends a pair $ \langle i, x \rangle $ to the element $ x $.

Set.sigmaToiUnion_surjective theorem

: Surjective (sigmaToiUnion t)

Full source

theorem sigmaToiUnion_surjective : Surjective (sigmaToiUnion t)
  | ⟨b, hb⟩ =>
    have : ∃ a, b ∈ t a := by simpa using hb
    let ⟨a, hb⟩ := this
    ⟨⟨a, b, hb⟩, rfl⟩

Surjectivity of the Natural Map from Dependent Sum to Union of Sets

Informal description

The natural map from the dependent sum type $\Sigma i, t_i$ to the union $\bigcup_i t_i$ is surjective. That is, for every element $x \in \bigcup_i t_i$, there exists an index $i$ and an element $y \in t_i$ such that $x = y$.

Set.sigmaToiUnion_injective theorem

(h : Pairwise (Disjoint on t)) : Injective (sigmaToiUnion t)

Full source

theorem sigmaToiUnion_injective (h : Pairwise (DisjointDisjoint on t)) :
    Injective (sigmaToiUnion t)
  | ⟨a₁, b₁, h₁⟩, ⟨a₂, b₂, h₂⟩, eq =>
    have b_eq : b₁ = b₂ := congr_arg Subtype.val eq
    have a_eq : a₁ = a₂ :=
      by_contradiction fun ne =>
        have : b₁ ∈ t a₁ ∩ t a₂ := ⟨h₁, b_eq.symm ▸ h₂⟩
        (h ne).le_bot this
    Sigma.eq a_eq <| Subtype.eq <| by subst b_eq; subst a_eq; rfl

Injectivity of the Dependent Sum to Union Map for Pairwise Disjoint Sets

Informal description

For an indexed family of sets $ t_i $ (where $ i $ belongs to some index set), if the sets are pairwise disjoint (i.e., $ t_i \cap t_j = \emptyset $ for all $ i \neq j $), then the natural map from the dependent sum type $ \Sigma i, t_i $ to the union $ \bigcup_i t_i $ is injective. In other words, if $ \langle i, x \rangle $ and $ \langle j, y \rangle $ are elements of $ \Sigma i, t_i $ such that $ x = y $ in $ \bigcup_i t_i $, then $ i = j $ and $ x = y $ in $ t_i $.

Set.sigmaToiUnion_bijective theorem

(h : Pairwise (Disjoint on t)) : Bijective (sigmaToiUnion t)

Full source

theorem sigmaToiUnion_bijective (h : Pairwise (DisjointDisjoint on t)) :
    Bijective (sigmaToiUnion t) :=
  ⟨sigmaToiUnion_injective t h, sigmaToiUnion_surjective t⟩

Bijectivity of the Dependent Sum to Union Map for Pairwise Disjoint Sets

Informal description

For an indexed family of sets $ t_i $ (where $ i $ belongs to some index set), if the sets are pairwise disjoint (i.e., $ t_i \cap t_j = \emptyset $ for all $ i \neq j $), then the natural map from the dependent sum type $ \Sigma i, t_i $ to the union $ \bigcup_i t_i $ is bijective. In other words, the map $ \langle i, x \rangle \mapsto x $ is both injective and surjective when the sets $ t_i $ are pairwise disjoint.

Set.sigmaEquiv definition

(s : α → Set β) (hs : ∀ b, ∃! i, b ∈ s i) : (Σ i, s i) ≃ β

Full source

/-- Equivalence from the disjoint union of a family of sets forming a partition of `β`, to `β`
itself. -/
noncomputable def sigmaEquiv (s : α → Set β) (hs : ∀ b, ∃! i, b ∈ s i) :
    (Σ i, s i) ≃ β where
  toFun | ⟨_, b⟩ => b
  invFun b := ⟨(hs b).choose, b, (hs b).choose_spec.1⟩
  left_inv | ⟨i, b, hb⟩ => Sigma.subtype_ext ((hs b).choose_spec.2 i hb).symm rfl
  right_inv _ := rfl

Bijection between disjoint union and base set for a partition

Informal description

Given an indexed family of sets $(s_i)_{i \in \alpha}$ in $\beta$ that forms a partition of $\beta$ (i.e., every element $b \in \beta$ belongs to exactly one $s_i$), there exists a bijection between the disjoint union $\Sigma i, s_i$ (where $\Sigma$ denotes the dependent sum type) and $\beta$ itself. The bijection maps each pair $(i, b)$ where $b \in s_i$ to $b$, and its inverse maps each $b \in \beta$ to the unique pair $(i, b)$ where $i$ is the unique index such that $b \in s_i$.

Set.unionEqSigmaOfDisjoint definition

{t : α → Set β} (h : Pairwise (Disjoint on t)) : (⋃ i, t i) ≃ Σ i, t i

Full source

/-- Equivalence between a disjoint union and a dependent sum. -/
noncomputable def unionEqSigmaOfDisjoint {t : α → Set β}
    (h : Pairwise (DisjointDisjoint on t)) :
    (⋃ i, t i) ≃ Σi, t i :=
  (Equiv.ofBijective _ <| sigmaToiUnion_bijective t h).symm

Bijection between union of pairwise disjoint sets and their dependent sum

Informal description

Given an indexed family of sets $ t_i $ (for $ i $ in some index set $ \alpha $) in a type $ \beta $, if the sets are pairwise disjoint (i.e., $ t_i \cap t_j = \emptyset $ for all $ i \neq j $), then the union $ \bigcup_i t_i $ is in bijection with the dependent sum type $ \Sigma i, t_i $. The bijection maps each element $ x $ in the union to the unique pair $ \langle i, x \rangle $ where $ x \in t_i $.

Set.iUnion_ge_eq_iUnion_nat_add theorem

(u : ℕ → Set α) (n : ℕ) : ⋃ i ≥ n, u i = ⋃ i, u (i + n)

Full source

theorem iUnion_ge_eq_iUnion_nat_add (u : ℕ → Set α) (n : ℕ) : ⋃ i ≥ n, u i = ⋃ i, u (i + n) :=
  iSup_ge_eq_iSup_nat_add u n

Union Shift Equality for Natural Numbers

Informal description

For any sequence of sets $(u_i)_{i \in \mathbb{N}}$ in a type $\alpha$ and any natural number $n$, the union of all sets $u_i$ with $i \geq n$ is equal to the union of the sets $u_{i+n}$ over all natural numbers $i$. In symbols: $$\bigcup_{i \geq n} u_i = \bigcup_{i} u_{i+n}$$

Set.iInter_ge_eq_iInter_nat_add theorem

(u : ℕ → Set α) (n : ℕ) : ⋂ i ≥ n, u i = ⋂ i, u (i + n)

Full source

theorem iInter_ge_eq_iInter_nat_add (u : ℕ → Set α) (n : ℕ) : ⋂ i ≥ n, u i = ⋂ i, u (i + n) :=
  iInf_ge_eq_iInf_nat_add u n

Intersection of Tail Sequence Equals Shifted Intersection

Informal description

For any sequence of sets $(u_i)_{i \in \mathbb{N}}$ indexed by natural numbers and any natural number $n$, the intersection of all sets $u_i$ with $i \geq n$ equals the intersection of all sets $u_{i+n}$ over all natural numbers $i$. In symbols: \[ \bigcap_{i \geq n} u_i = \bigcap_{i \in \mathbb{N}} u_{i+n} \]

Monotone.iUnion_nat_add theorem

{f : ℕ → Set α} (hf : Monotone f) (k : ℕ) : ⋃ n, f (n + k) = ⋃ n, f n

Full source

theorem _root_.Monotone.iUnion_nat_add {f : ℕ → Set α} (hf : Monotone f) (k : ℕ) :
    ⋃ n, f (n + k) = ⋃ n, f n :=
  hf.iSup_nat_add k

Union of Shifted Monotone Sequences of Sets Equals Original Union

Informal description

For any monotone sequence of sets $(f(n))_{n \in \mathbb{N}}$ and any natural number $k$, the union of the shifted sets $\bigcup_{n} f(n + k)$ is equal to the union of the original sets $\bigcup_{n} f(n)$.

Antitone.iInter_nat_add theorem

{f : ℕ → Set α} (hf : Antitone f) (k : ℕ) : ⋂ n, f (n + k) = ⋂ n, f n

Full source

theorem _root_.Antitone.iInter_nat_add {f : ℕ → Set α} (hf : Antitone f) (k : ℕ) :
    ⋂ n, f (n + k) = ⋂ n, f n :=
  hf.iInf_nat_add k

Intersection of Antitone Sequence of Sets is Invariant under Shift by $k$

Informal description

For any antitone sequence of sets $(f(n))_{n \in \mathbb{N}}$ in a type $\alpha$ and any natural number $k$, the intersection $\bigcap_{n} f(n + k)$ is equal to $\bigcap_{n} f(n)$.

Set.iUnion_iInter_ge_nat_add theorem

(f : ℕ → Set α) (k : ℕ) : ⋃ n, ⋂ i ≥ n, f (i + k) = ⋃ n, ⋂ i ≥ n, f i

Full source

@[simp]
theorem iUnion_iInter_ge_nat_add (f : ℕ → Set α) (k : ℕ) :
    ⋃ n, ⋂ i ≥ n, f (i + k) = ⋃ n, ⋂ i ≥ n, f i :=
  iSup_iInf_ge_nat_add f k

Shift Invariance of Liminf for Sequences of Sets

Informal description

For any sequence of sets $(f_n)_{n \in \mathbb{N}}$ in a type $\alpha$ and any natural number $k$, the union over $n$ of the intersections of $f_{i+k}$ for all $i \geq n$ is equal to the union over $n$ of the intersections of $f_i$ for all $i \geq n$. That is, $$ \bigcup_{n \in \mathbb{N}} \bigcap_{i \geq n} f_{i+k} = \bigcup_{n \in \mathbb{N}} \bigcap_{i \geq n} f_i. $$

Set.union_iUnion_nat_succ theorem

(u : ℕ → Set α) : (u 0 ∪ ⋃ i, u (i + 1)) = ⋃ i, u i

Full source

theorem union_iUnion_nat_succ (u : ℕ → Set α) : (u 0 ∪ ⋃ i, u (i + 1)) = ⋃ i, u i :=
  sup_iSup_nat_succ u

Union Decomposition for Sequence of Sets

Informal description

For any sequence of sets $(u_n)_{n \in \mathbb{N}}$ indexed by natural numbers, the union of the first set $u_0$ with the union of all subsequent sets $\bigcup_{i \in \mathbb{N}} u_{i+1}$ is equal to the union of all sets in the sequence $\bigcup_{i \in \mathbb{N}} u_i$. In symbols: $$ u_0 \cup \left( \bigcup_{i \in \mathbb{N}} u_{i+1} \right) = \bigcup_{i \in \mathbb{N}} u_i $$

Set.inter_iInter_nat_succ theorem

(u : ℕ → Set α) : (u 0 ∩ ⋂ i, u (i + 1)) = ⋂ i, u i

Full source

theorem inter_iInter_nat_succ (u : ℕ → Set α) : (u 0 ∩ ⋂ i, u (i + 1)) = ⋂ i, u i :=
  inf_iInf_nat_succ u

Intersection Identity for Shifted Sequence of Sets

Informal description

For any sequence of sets $(u_n)_{n \in \mathbb{N}}$ in a type $\alpha$, the intersection of $u_0$ with the intersection of all $u_{i+1}$ for $i \in \mathbb{N}$ equals the intersection of all $u_i$ for $i \in \mathbb{N}$. In symbols: $$ u_0 \cap \left(\bigcap_{i \in \mathbb{N}} u_{i+1}\right) = \bigcap_{i \in \mathbb{N}} u_i $$

iSup_iUnion theorem

(s : ι → Set α) (f : α → β) : ⨆ a ∈ ⋃ i, s i, f a = ⨆ (i) (a ∈ s i), f a

Full source

theorem iSup_iUnion (s : ι → Set α) (f : α → β) : ⨆ a ∈ ⋃ i, s i, f a = ⨆ (i) (a ∈ s i), f a := by
  rw [iSup_comm]
  simp_rw [mem_iUnion, iSup_exists]

Supremum over Union Equals Iterated Supremum

Informal description

For any indexed family of sets $s_i$ in a type $\alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the union $\bigcup_i s_i$ is equal to the supremum over all indices $i$ and all elements $a \in s_i$ of $f(a)$. In symbols: \[ \sup_{a \in \bigcup_i s_i} f(a) = \sup_{i} \sup_{a \in s_i} f(a) \]

iInf_iUnion theorem

(s : ι → Set α) (f : α → β) : ⨅ a ∈ ⋃ i, s i, f a = ⨅ (i) (a ∈ s i), f a

Full source

theorem iInf_iUnion (s : ι → Set α) (f : α → β) : ⨅ a ∈ ⋃ i, s i, f a = ⨅ (i) (a ∈ s i), f a :=
  iSup_iUnion (β := βᵒᵈ) s f

Infimum over Union Equals Iterated Infimum

Informal description

For any indexed family of sets $(s_i)_{i \in \iota}$ in a type $\alpha$ and any function $f : \alpha \to \beta$, the infimum of $f$ over the union $\bigcup_{i} s_i$ is equal to the infimum over all indices $i$ and all elements $a \in s_i$ of $f(a)$. In symbols: \[ \inf_{a \in \bigcup_i s_i} f(a) = \inf_{i} \inf_{a \in s_i} f(a) \]

sSup_iUnion theorem

(t : ι → Set β) : sSup (⋃ i, t i) = ⨆ i, sSup (t i)

Full source

theorem sSup_iUnion (t : ι → Set β) : sSup (⋃ i, t i) = ⨆ i, sSup (t i) := by
  simp_rw [sSup_eq_iSup, iSup_iUnion]

Supremum of Union Equals Supremum of Suprema

Informal description

For any indexed family of sets $t_i$ in a type $\beta$, the supremum of the union $\bigcup_i t_i$ is equal to the supremum over all indices $i$ of the supremum of $t_i$. In symbols: \[ \sup \left( \bigcup_i t_i \right) = \sup_i \left( \sup t_i \right) \]

sSup_sUnion theorem

(s : Set (Set β)) : sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

Full source

theorem sSup_sUnion (s : Set (Set β)) : sSup (⋃₀ s) = ⨆ t ∈ s, sSup t := by
  simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]

Supremum of Union of Sets Equals Supremum of Suprema

Informal description

For any collection of sets $s$ (where each element of $s$ is a subset of $\beta$), the supremum of the union $\bigcup₀ s$ is equal to the supremum over all sets $t \in s$ of the supremum of $t$. In symbols: \[ \sup \left( \bigcup₀ s \right) = \sup_{t \in s} \left( \sup t \right) \]

sInf_sUnion theorem

(s : Set (Set β)) : sInf (⋃₀ s) = ⨅ t ∈ s, sInf t

Full source

theorem sInf_sUnion (s : Set (Set β)) : sInf (⋃₀ s) = ⨅ t ∈ s, sInf t :=
  sSup_sUnion (β := βᵒᵈ) s

Infimum of Union of Sets Equals Infimum of Infima

Informal description

For any collection of sets $s$ (where each element of $s$ is a subset of $\beta$), the infimum of the union $\bigcup₀ s$ is equal to the infimum over all sets $t \in s$ of the infimum of $t$. In symbols: \[ \inf \left( \bigcup₀ s \right) = \inf_{t \in s} \left( \inf t \right) \]

iSup_sUnion theorem

(S : Set (Set α)) (f : α → β) : (⨆ x ∈ ⋃₀ S, f x) = ⨆ (s ∈ S) (x ∈ s), f x

Full source

lemma iSup_sUnion (S : Set (Set α)) (f : α → β) :
    (⨆ x ∈ ⋃₀ S, f x) = ⨆ (s ∈ S) (x ∈ s), f x := by
  rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']

Supremum over Union of Sets Equals Iterated Supremum

Informal description

For any collection of sets $S$ in a type $\alpha$ and any function $f : \alpha \to \beta$, the supremum of $f$ over the union $\bigcup₀ S$ is equal to the supremum over all sets $s \in S$ and all elements $x \in s$ of $f(x)$. In symbols: \[ \sup_{x \in \bigcup₀ S} f(x) = \sup_{s \in S} \sup_{x \in s} f(x) \]

iInf_sUnion theorem

(S : Set (Set α)) (f : α → β) : (⨅ x ∈ ⋃₀ S, f x) = ⨅ (s ∈ S) (x ∈ s), f x

Full source

lemma iInf_sUnion (S : Set (Set α)) (f : α → β) :
    (⨅ x ∈ ⋃₀ S, f x) = ⨅ (s ∈ S) (x ∈ s), f x := by
  rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

Infimum over Union of Sets Equals Iterated Infimum

Informal description

For any collection of sets $S$ in a type $\alpha$ and any function $f : \alpha \to \beta$, the infimum of $f$ over the union $\bigcup₀ S$ is equal to the infimum over all sets $s \in S$ and all elements $x \in s$ of $f(x)$. In symbols: \[ \inf_{x \in \bigcup₀ S} f(x) = \inf_{s \in S} \inf_{x \in s} f(x) \]

forall_sUnion theorem

{S : Set (Set α)} {p : α → Prop} : (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Full source

lemma forall_sUnion {S : Set (Set α)} {p : α → Prop} :
    (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x := by
  simp_rw [← iInf_Prop_eq, iInf_sUnion]

Universal Quantification over Union of Sets Equals Iterated Universal Quantification

Informal description

For any collection of sets $S$ in a type $\alpha$ and any predicate $p$ on $\alpha$, the predicate $p$ holds for all elements $x$ in the union $\bigcup₀ S$ if and only if for every set $s \in S$ and every element $x \in s$, the predicate $p(x)$ holds. In symbols: \[ (\forall x \in \bigcup₀ S, p(x)) \leftrightarrow (\forall s \in S, \forall x \in s, p(x)) \]

exists_sUnion theorem

{S : Set (Set α)} {p : α → Prop} : (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x

Full source

lemma exists_sUnion {S : Set (Set α)} {p : α → Prop} :
    (∃ x ∈ ⋃₀ S, p x) ↔ ∃ s ∈ S, ∃ x ∈ s, p x := by
  simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]

Existence in Union of Sets is Equivalent to Existence in Member Set

Informal description

For any collection of sets $S$ in a type $\alpha$ and any predicate $p$ on $\alpha$, there exists an element $x$ in the union $\bigcup₀ S$ satisfying $p(x)$ if and only if there exists a set $s \in S$ and an element $x \in s$ such that $p(x)$ holds. In symbols: \[ (\exists x \in \bigcup₀ S, p(x)) \leftrightarrow (\exists s \in S, \exists x \in s, p(x)) \]

Mathlib.Data.Set.Lattice

Main declarations

Naming convention

Notation