# The set lattice #

This file provides usual set notation for unions and intersections, a CompleteLattice instance for Set α, and some more set constructions.

## Main declarations #

• Set.iUnion: indexed union. Union of an indexed family of sets.
• Set.iInter: indexed intersection. Intersection of an indexed family of sets.
• Set.sInter: set intersection. Intersection of sets belonging to a set of sets.
• Set.sUnion: set union. Union of sets belonging to a set of sets.
• Set.sInter_eq_biInter, Set.sUnion_eq_biInter: Shows that ⋂₀ s = ⋂ x ∈ s, x and ⋃₀ s = ⋃ x ∈ s, x.
• Set.completeAtomicBooleanAlgebra: Set α is a CompleteAtomicBooleanAlgebra with ≤ = ⊆, < = ⊂, ⊓ = ∩, ⊔ = ∪, ⨅ = ⋂, ⨆ = ⋃ and \ as the set difference. See Set.BooleanAlgebra.
• Set.kernImage: For a function f : α → β, s.kernImage f is the set of y such that f ⁻¹ y ⊆ s.
• Set.seq: Union of the image of a set under a sequence of functions. seq s t is the union of f '' t over all f ∈ s, where t : Set α and s : Set (α → β).
• Set.unionEqSigmaOfDisjoint: Equivalence between ⋃ i, t i and Σ i, t i, where t is an indexed family of disjoint sets.

## Naming convention #

In lemma names,

• ⋃ i, s i is called iUnion
• ⋂ i, s i is called iInter
• ⋃ i j, s i j is called iUnion₂. This is an iUnion inside an iUnion.
• ⋂ i j, s i j is called iInter₂. This is an iInter inside an iInter.
• ⋃ i ∈ s, t i is called biUnion for "bounded iUnion". This is the special case of iUnion₂ where j : i ∈ s.
• ⋂ i ∈ s, t i is called biInter for "bounded iInter". This is the special case of iInter₂ where j : i ∈ s.

## Notation #

• ⋃: Set.iUnion
• ⋂: Set.iInter
• ⋃₀: Set.sUnion
• ⋂₀: Set.sInter

### Complete lattice and complete Boolean algebra instances #

theorem Set.mem_iUnion₂ {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_7} {x : γ} {s : (i : ι) → κ iSet γ} :
x ⋃ (i : ι), ⋃ (j : κ i), s i j ∃ (i : ι) (j : κ i), x s i j
theorem Set.mem_iInter₂ {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_7} {x : γ} {s : (i : ι) → κ iSet γ} :
x ⋂ (i : ι), ⋂ (j : κ i), s i j ∀ (i : ι) (j : κ i), x s i j
theorem Set.mem_iUnion_of_mem {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {a : α} (i : ι) (ha : a s i) :
a ⋃ (i : ι), s i
theorem Set.mem_iUnion₂_of_mem {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {a : α} {i : ι} (j : κ i) (ha : a s i j) :
a ⋃ (i : ι), ⋃ (j : κ i), s i j
theorem Set.mem_iInter_of_mem {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {a : α} (h : ∀ (i : ι), a s i) :
a ⋂ (i : ι), s i
theorem Set.mem_iInter₂_of_mem {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {a : α} (h : ∀ (i : ι) (j : κ i), a s i j) :
a ⋂ (i : ι), ⋂ (j : κ i), s i j
Equations
• Set.completeAtomicBooleanAlgebra =
theorem Set.image_preimage {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem Set.preimage_kernImage {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem Set.kernImage_mono {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem Set.kernImage_eq_compl {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
= (f '' s)
theorem Set.kernImage_compl {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
= (f '' s)
theorem Set.kernImage_empty {α : Type u_1} {β : Type u_2} {f : αβ} :
theorem Set.kernImage_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set β} :
theorem Set.compl_range_subset_kernImage {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} :
theorem Set.kernImage_union_preimage {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set β} :
theorem Set.kernImage_preimage_union {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set α} {t : Set β} :

### Union and intersection over an indexed family of sets #

instance Set.instOrderTop {α : Type u_1} :
Equations
• Set.instOrderTop =
theorem Set.iUnion_congr_Prop {α : Type u_1} {p : Prop} {q : Prop} {f₁ : pSet α} {f₂ : qSet α} (pq : p q) (f : ∀ (x : q), f₁ = f₂ x) :
=
theorem Set.iInter_congr_Prop {α : Type u_1} {p : Prop} {q : Prop} {f₁ : pSet α} {f₂ : qSet α} (pq : p q) (f : ∀ (x : q), f₁ = f₂ x) :
=
theorem Set.iUnion_plift_up {α : Type u_1} {ι : Sort u_4} (f : Set α) :
⋃ (i : ι), f { down := i } = ⋃ (i : ), f i
theorem Set.iUnion_plift_down {α : Type u_1} {ι : Sort u_4} (f : ιSet α) :
⋃ (i : ), f i.down = ⋃ (i : ι), f i
theorem Set.iInter_plift_up {α : Type u_1} {ι : Sort u_4} (f : Set α) :
⋂ (i : ι), f { down := i } = ⋂ (i : ), f i
theorem Set.iInter_plift_down {α : Type u_1} {ι : Sort u_4} (f : ιSet α) :
⋂ (i : ), f i.down = ⋂ (i : ι), f i
theorem Set.iUnion_eq_if {α : Type u_1} {p : Prop} [] (s : Set α) :
⋃ (_ : p), s = if p then s else
theorem Set.iUnion_eq_dif {α : Type u_1} {p : Prop} [] (s : pSet α) :
⋃ (h : p), s h = if h : p then s h else
theorem Set.iInter_eq_if {α : Type u_1} {p : Prop} [] (s : Set α) :
⋂ (_ : p), s = if p then s else Set.univ
theorem Set.iInf_eq_dif {α : Type u_1} {p : Prop} [] (s : pSet α) :
⋂ (h : p), s h = if h : p then s h else Set.univ
theorem Set.exists_set_mem_of_union_eq_top {β : Type u_2} {ι : Type u_11} (t : Set ι) (s : ιSet β) (w : it, s i = ) (x : β) :
it, x s i
theorem Set.nonempty_of_union_eq_top_of_nonempty {α : Type u_1} {ι : Type u_11} (t : Set ι) (s : ιSet α) (H : ) (w : it, s i = ) :
t.Nonempty
theorem Set.nonempty_of_nonempty_iUnion {α : Type u_1} {ι : Sort u_4} {s : ιSet α} (h_Union : (⋃ (i : ι), s i).Nonempty) :
theorem Set.nonempty_of_nonempty_iUnion_eq_univ {α : Type u_1} {ι : Sort u_4} {s : ιSet α} [] (h_Union : ⋃ (i : ι), s i = Set.univ) :
theorem Set.setOf_exists {β : Type u_2} {ι : Sort u_4} (p : ιβProp) :
{x : β | ∃ (i : ι), p i x} = ⋃ (i : ι), {x : β | p i x}
theorem Set.setOf_forall {β : Type u_2} {ι : Sort u_4} (p : ιβProp) :
{x : β | ∀ (i : ι), p i x} = ⋂ (i : ι), {x : β | p i x}
theorem Set.iUnion_subset {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : Set α} (h : ∀ (i : ι), s i t) :
⋃ (i : ι), s i t
theorem Set.iUnion₂_subset {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : Set α} (h : ∀ (i : ι) (j : κ i), s i j t) :
⋃ (i : ι), ⋃ (j : κ i), s i j t
theorem Set.subset_iInter {β : Type u_2} {ι : Sort u_4} {t : Set β} {s : ιSet β} (h : ∀ (i : ι), t s i) :
t ⋂ (i : ι), s i
theorem Set.subset_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s t i j) :
s ⋂ (i : ι), ⋂ (j : κ i), t i j
@[simp]
theorem Set.iUnion_subset_iff {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : Set α} :
⋃ (i : ι), s i t ∀ (i : ι), s i t
theorem Set.iUnion₂_subset_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : Set α} :
⋃ (i : ι), ⋃ (j : κ i), s i j t ∀ (i : ι) (j : κ i), s i j t
@[simp]
theorem Set.subset_iInter_iff {α : Type u_1} {ι : Sort u_4} {s : Set α} {t : ιSet α} :
s ⋂ (i : ι), t i ∀ (i : ι), s t i
theorem Set.subset_iInter₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet α} :
s ⋂ (i : ι), ⋂ (j : κ i), t i j ∀ (i : ι) (j : κ i), s t i j
theorem Set.subset_iUnion {β : Type u_2} {ι : Sort u_4} (s : ιSet β) (i : ι) :
s i ⋃ (i : ι), s i
theorem Set.iInter_subset {β : Type u_2} {ι : Sort u_4} (s : ιSet β) (i : ι) :
⋂ (i : ι), s i s i
theorem Set.subset_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} (i : ι) (j : κ i) :
s i j ⋃ (i' : ι), ⋃ (j' : κ i'), s i' j'
theorem Set.iInter₂_subset {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} (i : ι) (j : κ i) :
⋂ (i : ι), ⋂ (j : κ i), s i j s i j
theorem Set.subset_iUnion_of_subset {α : Type u_1} {ι : Sort u_4} {s : Set α} {t : ιSet α} (i : ι) (h : s t i) :
s ⋃ (i : ι), t i

This rather trivial consequence of subset_iUnionis convenient with apply, and has i explicit for this purpose.

theorem Set.iInter_subset_of_subset {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : Set α} (i : ι) (h : s i t) :
⋂ (i : ι), s i t

This rather trivial consequence of iInter_subsetis convenient with apply, and has i explicit for this purpose.

theorem Set.subset_iUnion₂_of_subset {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet α} (i : ι) (j : κ i) (h : s t i j) :
s ⋃ (i : ι), ⋃ (j : κ i), t i j

This rather trivial consequence of subset_iUnion₂ is convenient with apply, and has i and j explicit for this purpose.

theorem Set.iInter₂_subset_of_subset {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : Set α} (i : ι) (j : κ i) (h : s i j t) :
⋂ (i : ι), ⋂ (j : κ i), s i j t

This rather trivial consequence of iInter₂_subset is convenient with apply, and has i and j explicit for this purpose.

theorem Set.iUnion_mono {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i t i) :
⋃ (i : ι), s i ⋃ (i : ι), t i
theorem Set.iUnion_mono'' {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i t i) :
theorem Set.iUnion₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j t i j) :
⋃ (i : ι), ⋃ (j : κ i), s i j ⋃ (i : ι), ⋃ (j : κ i), t i j
theorem Set.iInter_mono {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i t i) :
⋂ (i : ι), s i ⋂ (i : ι), t i
theorem Set.iInter_mono'' {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i t i) :
theorem Set.iInter₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j t i j) :
⋂ (i : ι), ⋂ (j : κ i), s i j ⋂ (i : ι), ⋂ (j : κ i), t i j
theorem Set.iUnion_mono' {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : ιSet α} {t : ι₂Set α} (h : ∀ (i : ι), ∃ (j : ι₂), s i t j) :
⋃ (i : ι), s i ⋃ (i : ι₂), t i
theorem Set.iUnion₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ιSort u_7} {κ' : ι'Sort u_10} {s : (i : ι) → κ iSet α} {t : (i' : ι') → κ' i'Set α} (h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), s i j t i' j') :
⋃ (i : ι), ⋃ (j : κ i), s i j ⋃ (i' : ι'), ⋃ (j' : κ' i'), t i' j'
theorem Set.iInter_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {s : ιSet α} {t : ι'Set α} (h : ∀ (j : ι'), ∃ (i : ι), s i t j) :
⋂ (i : ι), s i ⋂ (j : ι'), t j
theorem Set.iInter₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ιSort u_7} {κ' : ι'Sort u_10} {s : (i : ι) → κ iSet α} {t : (i' : ι') → κ' i'Set α} (h : ∀ (i' : ι') (j' : κ' i'), ∃ (i : ι) (j : κ i), s i j t i' j') :
⋂ (i : ι), ⋂ (j : κ i), s i j ⋂ (i' : ι'), ⋂ (j' : κ' i'), t i' j'
theorem Set.iUnion₂_subset_iUnion {α : Type u_1} {ι : Sort u_4} (κ : ιSort u_11) (s : ιSet α) :
⋃ (i : ι), ⋃ (x : κ i), s i ⋃ (i : ι), s i
theorem Set.iInter_subset_iInter₂ {α : Type u_1} {ι : Sort u_4} (κ : ιSort u_11) (s : ιSet α) :
⋂ (i : ι), s i ⋂ (i : ι), ⋂ (x : κ i), s i
theorem Set.iUnion_setOf {α : Type u_1} {ι : Sort u_4} (P : ιαProp) :
⋃ (i : ι), {x : α | P i x} = {x : α | ∃ (i : ι), P i x}
theorem Set.iInter_setOf {α : Type u_1} {ι : Sort u_4} (P : ιαProp) :
⋂ (i : ι), {x : α | P i x} = {x : α | ∀ (i : ι), P i x}
theorem Set.iUnion_congr_of_surjective {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ιSet α} {g : ι₂Set α} (h : ιι₂) (h1 : ) (h2 : ∀ (x : ι), g (h x) = f x) :
⋃ (x : ι), f x = ⋃ (y : ι₂), g y
theorem Set.iInter_congr_of_surjective {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ιSet α} {g : ι₂Set α} (h : ιι₂) (h1 : ) (h2 : ∀ (x : ι), g (h x) = f x) :
⋂ (x : ι), f x = ⋂ (y : ι₂), g y
theorem Set.iUnion_congr {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i = t i) :
⋃ (i : ι), s i = ⋃ (i : ι), t i
theorem Set.iInter_congr {α : Type u_1} {ι : Sort u_4} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i = t i) :
⋂ (i : ι), s i = ⋂ (i : ι), t i
theorem Set.iUnion₂_congr {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j = t i j) :
⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), t i j
theorem Set.iInter₂_congr {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j = t i j) :
⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), t i j
theorem Set.iUnion_const {β : Type u_2} {ι : Sort u_4} [] (s : Set β) :
⋃ (x : ι), s = s
theorem Set.iInter_const {β : Type u_2} {ι : Sort u_4} [] (s : Set β) :
⋂ (x : ι), s = s
theorem Set.iUnion_eq_const {α : Type u_1} {ι : Sort u_4} [] {f : ιSet α} {s : Set α} (hf : ∀ (i : ι), f i = s) :
⋃ (i : ι), f i = s
theorem Set.iInter_eq_const {α : Type u_1} {ι : Sort u_4} [] {f : ιSet α} {s : Set α} (hf : ∀ (i : ι), f i = s) :
⋂ (i : ι), f i = s
@[simp]
theorem Set.compl_iUnion {β : Type u_2} {ι : Sort u_4} (s : ιSet β) :
(⋃ (i : ι), s i) = ⋂ (i : ι), (s i)
theorem Set.compl_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : (i : ι) → κ iSet α) :
(⋃ (i : ι), ⋃ (j : κ i), s i j) = ⋂ (i : ι), ⋂ (j : κ i), (s i j)
@[simp]
theorem Set.compl_iInter {β : Type u_2} {ι : Sort u_4} (s : ιSet β) :
(⋂ (i : ι), s i) = ⋃ (i : ι), (s i)
theorem Set.compl_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : (i : ι) → κ iSet α) :
(⋂ (i : ι), ⋂ (j : κ i), s i j) = ⋃ (i : ι), ⋃ (j : κ i), (s i j)
theorem Set.iUnion_eq_compl_iInter_compl {β : Type u_2} {ι : Sort u_4} (s : ιSet β) :
⋃ (i : ι), s i = (⋂ (i : ι), (s i))
theorem Set.iInter_eq_compl_iUnion_compl {β : Type u_2} {ι : Sort u_4} (s : ιSet β) :
⋂ (i : ι), s i = (⋃ (i : ι), (s i))
theorem Set.inter_iUnion {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ιSet β) :
s ⋃ (i : ι), t i = ⋃ (i : ι), s t i
theorem Set.iUnion_inter {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ιSet β) :
(⋃ (i : ι), t i) s = ⋃ (i : ι), t i s
theorem Set.iUnion_union_distrib {β : Type u_2} {ι : Sort u_4} (s : ιSet β) (t : ιSet β) :
⋃ (i : ι), s i t i = (⋃ (i : ι), s i) ⋃ (i : ι), t i
theorem Set.iInter_inter_distrib {β : Type u_2} {ι : Sort u_4} (s : ιSet β) (t : ιSet β) :
⋂ (i : ι), s i t i = (⋂ (i : ι), s i) ⋂ (i : ι), t i
theorem Set.union_iUnion {β : Type u_2} {ι : Sort u_4} [] (s : Set β) (t : ιSet β) :
s ⋃ (i : ι), t i = ⋃ (i : ι), s t i
theorem Set.iUnion_union {β : Type u_2} {ι : Sort u_4} [] (s : Set β) (t : ιSet β) :
(⋃ (i : ι), t i) s = ⋃ (i : ι), t i s
theorem Set.inter_iInter {β : Type u_2} {ι : Sort u_4} [] (s : Set β) (t : ιSet β) :
s ⋂ (i : ι), t i = ⋂ (i : ι), s t i
theorem Set.iInter_inter {β : Type u_2} {ι : Sort u_4} [] (s : Set β) (t : ιSet β) :
(⋂ (i : ι), t i) s = ⋂ (i : ι), t i s
theorem Set.union_iInter {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ιSet β) :
s ⋂ (i : ι), t i = ⋂ (i : ι), s t i
theorem Set.iInter_union {β : Type u_2} {ι : Sort u_4} (s : ιSet β) (t : Set β) :
(⋂ (i : ι), s i) t = ⋂ (i : ι), s i t
theorem Set.iUnion_diff {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ιSet β) :
(⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s
theorem Set.diff_iUnion {β : Type u_2} {ι : Sort u_4} [] (s : Set β) (t : ιSet β) :
s \ ⋃ (i : ι), t i = ⋂ (i : ι), s \ t i
theorem Set.diff_iInter {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ιSet β) :
s \ ⋂ (i : ι), t i = ⋃ (i : ι), s \ t i
theorem Set.iUnion_inter_subset {ι : Sort u_11} {α : Type u_12} {s : ιSet α} {t : ιSet α} :
⋃ (i : ι), s i t i (⋃ (i : ι), s i) ⋃ (i : ι), t i
theorem Set.iUnion_inter_of_monotone {ι : Type u_11} {α : Type u_12} [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
⋃ (i : ι), s i t i = (⋃ (i : ι), s i) ⋃ (i : ι), t i
theorem Set.iUnion_inter_of_antitone {ι : Type u_11} {α : Type u_12} [] [IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 x2)] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
⋃ (i : ι), s i t i = (⋃ (i : ι), s i) ⋃ (i : ι), t i
theorem Set.iInter_union_of_monotone {ι : Type u_11} {α : Type u_12} [] [IsDirected ι (Function.swap fun (x1 x2 : ι) => x1 x2)] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
⋂ (i : ι), s i t i = (⋂ (i : ι), s i) ⋂ (i : ι), t i
theorem Set.iInter_union_of_antitone {ι : Type u_11} {α : Type u_12} [] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
⋂ (i : ι), s i t i = (⋂ (i : ι), s i) ⋂ (i : ι), t i
theorem Set.iUnion_iInter_subset {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {s : ιι'Set α} :
⋃ (j : ι'), ⋂ (i : ι), s i j ⋂ (i : ι), ⋃ (j : ι'), s i j

An equality version of this lemma is iUnion_iInter_of_monotone in Data.Set.Finite.

theorem Set.iUnion_option {α : Type u_1} {ι : Type u_11} (s : Set α) :
⋃ (o : ), s o = s none ⋃ (i : ι), s (some i)
theorem Set.iInter_option {α : Type u_1} {ι : Type u_11} (s : Set α) :
⋂ (o : ), s o = s none ⋂ (i : ι), s (some i)
theorem Set.iUnion_dite {α : Type u_1} {ι : Sort u_4} (p : ιProp) [] (f : (i : ι) → p iSet α) (g : (i : ι) → ¬p iSet α) :
(⋃ (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
theorem Set.iUnion_ite {α : Type u_1} {ι : Sort u_4} (p : ιProp) [] (f : ιSet α) (g : ιSet α) :
(⋃ (i : ι), if p i then f i else g i) = (⋃ (i : ι), ⋃ (_ : p i), f i) ⋃ (i : ι), ⋃ (_ : ¬p i), g i
theorem Set.iInter_dite {α : Type u_1} {ι : Sort u_4} (p : ιProp) [] (f : (i : ι) → p iSet α) (g : (i : ι) → ¬p iSet α) :
(⋂ (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
theorem Set.iInter_ite {α : Type u_1} {ι : Sort u_4} (p : ιProp) [] (f : ιSet α) (g : ιSet α) :
(⋂ (i : ι), if p i then f i else g i) = (⋂ (i : ι), ⋂ (_ : p i), f i) ⋂ (i : ι), ⋂ (_ : ¬p i), g i
theorem Set.image_projection_prod {ι : Type u_11} {α : ιType u_12} {v : (i : ι) → Set (α i)} (hv : (Set.univ.pi v).Nonempty) (i : ι) :
(fun (x : (i : ι) → α i) => x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) => x k) ⁻¹' v k = v i

### Unions and intersections indexed by Prop#

theorem Set.iInter_false {α : Type u_1} {s : FalseSet α} :
= Set.univ
theorem Set.iUnion_false {α : Type u_1} {s : FalseSet α} :
@[simp]
theorem Set.iInter_true {α : Type u_1} {s : TrueSet α} :
@[simp]
theorem Set.iUnion_true {α : Type u_1} {s : TrueSet α} :
@[simp]
theorem Set.iInter_exists {α : Type u_1} {ι : Sort u_4} {p : ιProp} {f : Set α} :
⋂ (x : ), f x = ⋂ (i : ι), ⋂ (h : p i), f
@[simp]
theorem Set.iUnion_exists {α : Type u_1} {ι : Sort u_4} {p : ιProp} {f : Set α} :
⋃ (x : ), f x = ⋃ (i : ι), ⋃ (h : p i), f
@[simp]
theorem Set.iUnion_empty {α : Type u_1} {ι : Sort u_4} :
⋃ (x : ι), =
@[simp]
theorem Set.iInter_univ {α : Type u_1} {ι : Sort u_4} :
⋂ (x : ι), Set.univ = Set.univ
@[simp]
theorem Set.iUnion_eq_empty {α : Type u_1} {ι : Sort u_4} {s : ιSet α} :
⋃ (i : ι), s i = ∀ (i : ι), s i =
@[simp]
theorem Set.iInter_eq_univ {α : Type u_1} {ι : Sort u_4} {s : ιSet α} :
⋂ (i : ι), s i = Set.univ ∀ (i : ι), s i = Set.univ
@[simp]
theorem Set.nonempty_iUnion {α : Type u_1} {ι : Sort u_4} {s : ιSet α} :
(⋃ (i : ι), s i).Nonempty ∃ (i : ι), (s i).Nonempty
theorem Set.nonempty_biUnion {α : Type u_1} {β : Type u_2} {t : Set α} {s : αSet β} :
(⋃ it, s i).Nonempty it, (s i).Nonempty
theorem Set.iUnion_nonempty_index {α : Type u_1} {β : Type u_2} (s : Set α) (t : s.NonemptySet β) :
⋃ (h : s.Nonempty), t h = ⋃ (x : α), ⋃ (h : x s), t
@[simp]
theorem Set.iInter_iInter_eq_left {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → x = bSet α} :
⋂ (x : β), ⋂ (h : x = b), s x h = s b
@[simp]
theorem Set.iInter_iInter_eq_right {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = xSet α} :
⋂ (x : β), ⋂ (h : b = x), s x h = s b
@[simp]
theorem Set.iUnion_iUnion_eq_left {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → x = bSet α} :
⋃ (x : β), ⋃ (h : x = b), s x h = s b
@[simp]
theorem Set.iUnion_iUnion_eq_right {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = xSet α} :
⋃ (x : β), ⋃ (h : b = x), s x h = s b
theorem Set.iInter_or {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
⋂ (h : p q), s h = (⋂ (h : p), s ) ⋂ (h : q), s
theorem Set.iUnion_or {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
⋃ (h : p q), s h = (⋃ (i : p), s ) ⋃ (j : q), s
theorem Set.iUnion_and {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
⋃ (h : p q), s h = ⋃ (hp : p), ⋃ (hq : q), s
theorem Set.iInter_and {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
⋂ (h : p q), s h = ⋂ (hp : p), ⋂ (hq : q), s
theorem Set.iUnion_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (s : ιι'Set α) :
⋃ (i : ι), ⋃ (i' : ι'), s i i' = ⋃ (i' : ι'), ⋃ (i : ι), s i i'
theorem Set.iInter_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (s : ιι'Set α) :
⋂ (i : ι), ⋂ (i' : ι'), s i i' = ⋂ (i' : ι'), ⋂ (i : ι), s i i'
theorem Set.iUnion_sigma {α : Type u_1} {β : Type u_2} {γ : αType u_11} (s : Set β) :
⋃ (ia : ), s ia = ⋃ (i : α), ⋃ (a : γ i), s i, a
theorem Set.iUnion_sigma' {α : Type u_1} {β : Type u_2} {γ : αType u_11} (s : (i : α) → γ iSet β) :
⋃ (i : α), ⋃ (a : γ i), s i a = ⋃ (ia : ), s ia.fst ia.snd
theorem Set.iInter_sigma {α : Type u_1} {β : Type u_2} {γ : αType u_11} (s : Set β) :
⋂ (ia : ), s ia = ⋂ (i : α), ⋂ (a : γ i), s i, a
theorem Set.iInter_sigma' {α : Type u_1} {β : Type u_2} {γ : αType u_11} (s : (i : α) → γ iSet β) :
⋂ (i : α), ⋂ (a : γ i), s i a = ⋂ (ia : ), s ia.fst ia.snd
theorem Set.iUnion₂_comm {α : Type u_1} {ι : Sort u_4} {κ₁ : ιSort u_8} {κ₂ : ιSort u_9} (s : (i₁ : ι) → κ₁ i₁(i₂ : ι) → κ₂ i₂Set α) :
⋃ (i₁ : ι), ⋃ (j₁ : κ₁ i₁), ⋃ (i₂ : ι), ⋃ (j₂ : κ₂ i₂), s i₁ j₁ i₂ j₂ = ⋃ (i₂ : ι), ⋃ (j₂ : κ₂ i₂), ⋃ (i₁ : ι), ⋃ (j₁ : κ₁ i₁), s i₁ j₁ i₂ j₂
theorem Set.iInter₂_comm {α : Type u_1} {ι : Sort u_4} {κ₁ : ιSort u_8} {κ₂ : ιSort u_9} (s : (i₁ : ι) → κ₁ i₁(i₂ : ι) → κ₂ i₂Set α) :
⋂ (i₁ : ι), ⋂ (j₁ : κ₁ i₁), ⋂ (i₂ : ι), ⋂ (j₂ : κ₂ i₂), s i₁ j₁ i₂ j₂ = ⋂ (i₂ : ι), ⋂ (j₂ : κ₂ i₂), ⋂ (i₁ : ι), ⋂ (j₁ : κ₁ i₁), s i₁ j₁ i₂ j₂
@[simp]
theorem Set.biUnion_and {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ιProp) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p x q x ySet α) :
⋃ (x : ι), ⋃ (y : ι'), ⋃ (h : p x q x y), s x y h = ⋃ (x : ι), ⋃ (hx : p x), ⋃ (y : ι'), ⋃ (hy : q x y), s x y
@[simp]
theorem Set.biUnion_and' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι'Prop) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p y q x ySet α) :
⋃ (x : ι), ⋃ (y : ι'), ⋃ (h : p y q x y), s x y h = ⋃ (y : ι'), ⋃ (hy : p y), ⋃ (x : ι), ⋃ (hx : q x y), s x y
@[simp]
theorem Set.biInter_and {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ιProp) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p x q x ySet α) :
⋂ (x : ι), ⋂ (y : ι'), ⋂ (h : p x q x y), s x y h = ⋂ (x : ι), ⋂ (hx : p x), ⋂ (y : ι'), ⋂ (hy : q x y), s x y
@[simp]
theorem Set.biInter_and' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (p : ι'Prop) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p y q x ySet α) :
⋂ (x : ι), ⋂ (y : ι'), ⋂ (h : p y q x y), s x y h = ⋂ (y : ι'), ⋂ (hy : p y), ⋂ (x : ι), ⋂ (hx : q x y), s x y
@[simp]
theorem Set.iUnion_iUnion_eq_or_left {α : Type u_1} {β : Type u_2} {b : β} {p : βProp} {s : (x : β) → x = b p xSet α} :
⋃ (x : β), ⋃ (h : x = b p x), s x h = s b ⋃ (x : β), ⋃ (h : p x), s x
@[simp]
theorem Set.iInter_iInter_eq_or_left {α : Type u_1} {β : Type u_2} {b : β} {p : βProp} {s : (x : β) → x = b p xSet α} :
⋂ (x : β), ⋂ (h : x = b p x), s x h = s b ⋂ (x : β), ⋂ (h : p x), s x
theorem Set.iUnion_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : α βSet γ} :
⋃ (x : α β), s x = (⋃ (x : α), s (Sum.inl x)) ⋃ (x : β), s (Sum.inr x)
theorem Set.iInter_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : α βSet γ} :
⋂ (x : α β), s x = (⋂ (x : α), s (Sum.inl x)) ⋂ (x : β), s (Sum.inr x)

### Bounded unions and intersections #

theorem Set.mem_biUnion {α : Type u_1} {β : Type u_2} {s : Set α} {t : αSet β} {x : α} {y : β} (xs : x s) (ytx : y t x) :
y xs, t x

A specialization of mem_iUnion₂.

theorem Set.mem_biInter {α : Type u_1} {β : Type u_2} {s : Set α} {t : αSet β} {y : β} (h : xs, y t x) :
y xs, t x

A specialization of mem_iInter₂.

theorem Set.subset_biUnion_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {u : αSet β} {x : α} (xs : x s) :
u x xs, u x

A specialization of subset_iUnion₂.

theorem Set.biInter_subset_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {t : αSet β} {x : α} (xs : x s) :
xs, t x t x

A specialization of iInter₂_subset.

theorem Set.biUnion_subset_biUnion_left {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} (h : s s') :
xs, t x xs', t x
theorem Set.biInter_subset_biInter_left {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} (h : s' s) :
xs, t x xs', t x
theorem Set.biUnion_mono {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} {t' : αSet β} (hs : s' s) (h : xs, t x t' x) :
xs', t x xs, t' x
theorem Set.biInter_mono {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} {t' : αSet β} (hs : s s') (h : xs, t x t' x) :
xs', t x xs, t' x
theorem Set.biUnion_eq_iUnion {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x sSet β) :
⋃ (x : α), ⋃ (h : x s), t x h = ⋃ (x : s), t x
theorem Set.biInter_eq_iInter {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x sSet β) :
⋂ (x : α), ⋂ (h : x s), t x h = ⋂ (x : s), t x
theorem Set.iUnion_subtype {α : Type u_1} {β : Type u_2} (p : αProp) (s : { x : α // p x }Set β) :
⋃ (x : { x : α // p x }), s x = ⋃ (x : α), ⋃ (hx : p x), s x, hx
theorem Set.iInter_subtype {α : Type u_1} {β : Type u_2} (p : αProp) (s : { x : α // p x }Set β) :
⋂ (x : { x : α // p x }), s x = ⋂ (x : α), ⋂ (hx : p x), s x, hx
theorem Set.biInter_empty {α : Type u_1} {β : Type u_2} (u : αSet β) :
x, u x = Set.univ
theorem Set.biInter_univ {α : Type u_1} {β : Type u_2} (u : αSet β) :
xSet.univ, u x = ⋂ (x : α), u x
@[simp]
theorem Set.biUnion_self {α : Type u_1} (s : Set α) :
xs, s = s
@[simp]
theorem Set.iUnion_nonempty_self {α : Type u_1} (s : Set α) :
⋃ (_ : s.Nonempty), s = s
theorem Set.biInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : αSet β) :
x{a}, s x = s a
theorem Set.biInter_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : αSet β) :
xs t, u x = (⋂ xs, u x) xt, u x
theorem Set.biInter_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : αSet β) :
xinsert a s, t x = t a xs, t x
theorem Set.biInter_pair {α : Type u_1} {β : Type u_2} (a : α) (b : α) (s : αSet β) :
x{a, b}, s x = s a s b
theorem Set.biInter_inter {ι : Type u_11} {α : Type u_12} {s : Set ι} (hs : s.Nonempty) (f : ιSet α) (t : Set α) :
is, f i t = (⋂ is, f i) t
theorem Set.inter_biInter {ι : Type u_11} {α : Type u_12} {s : Set ι} (hs : s.Nonempty) (f : ιSet α) (t : Set α) :
is, t f i = t is, f i
theorem Set.biUnion_empty {α : Type u_1} {β : Type u_2} (s : αSet β) :
x, s x =
theorem Set.biUnion_univ {α : Type u_1} {β : Type u_2} (s : αSet β) :
xSet.univ, s x = ⋃ (x : α), s x
theorem Set.biUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : αSet β) :
x{a}, s x = s a
@[simp]
theorem Set.biUnion_of_singleton {α : Type u_1} (s : Set α) :
xs, {x} = s
theorem Set.biUnion_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : αSet β) :
xs t, u x = (⋃ xs, u x) xt, u x
@[simp]
theorem Set.iUnion_coe_set {α : Type u_11} {β : Type u_12} (s : Set α) (f : sSet β) :
⋃ (i : s), f i = ⋃ (i : α), ⋃ (h : i s), f i, h
@[simp]
theorem Set.iInter_coe_set {α : Type u_11} {β : Type u_12} (s : Set α) (f : sSet β) :
⋂ (i : s), f i = ⋂ (i : α), ⋂ (h : i s), f i, h
theorem Set.biUnion_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : αSet β) :
xinsert a s, t x = t a xs, t x
theorem Set.biUnion_pair {α : Type u_1} {β : Type u_2} (a : α) (b : α) (s : αSet β) :
x{a, b}, s x = s a s b
theorem Set.inter_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : Set α) (t : (i : ι) → κ iSet α) :
s ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s t i j
theorem Set.iUnion₂_inter {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : (i : ι) → κ iSet α) (t : Set α) :
(⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), s i j t
theorem Set.union_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : Set α) (t : (i : ι) → κ iSet α) :
s ⋂ (i : ι), ⋂ (j : κ i), t i j = ⋂ (i : ι), ⋂ (j : κ i), s t i j
theorem Set.iInter₂_union {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : (i : ι) → κ iSet α) (t : Set α) :
(⋂ (i : ι), ⋂ (j : κ i), s i j) t = ⋂ (i : ι), ⋂ (j : κ i), s i j t
theorem Set.mem_sUnion_of_mem {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)} (hx : x t) (ht : t S) :
theorem Set.not_mem_of_not_mem_sUnion {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)} (hx : x⋃₀ S) (ht : t S) :
xt
theorem Set.sInter_subset_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t S) :
theorem Set.subset_sUnion_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t S) :
theorem Set.subset_sUnion_of_subset {α : Type u_1} {s : Set α} (t : Set (Set α)) (u : Set α) (h₁ : s u) (h₂ : u t) :
theorem Set.sUnion_subset {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : t'S, t' t) :
@[simp]
theorem Set.sUnion_subset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} :
⋃₀ s t t's, t' t
theorem Set.sUnion_mono_subsets {α : Type u_1} {s : Set (Set α)} {f : Set αSet α} (hf : ∀ (t : Set α), t f t) :

sUnion is monotone under taking a subset of each set.

theorem Set.sUnion_mono_supsets {α : Type u_1} {s : Set (Set α)} {f : Set αSet α} (hf : ∀ (t : Set α), f t t) :

sUnion is monotone under taking a superset of each set.

theorem Set.subset_sInter {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : t'S, t t') :
@[simp]
theorem Set.subset_sInter_iff {α : Type u_1} {S : Set (Set α)} {t : Set α} :
t ⋂₀ S t'S, t t'
theorem Set.sUnion_subset_sUnion {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S T) :
theorem Set.sInter_subset_sInter {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S T) :
@[simp]
theorem Set.sUnion_empty {α : Type u_1} :
@[simp]
theorem Set.sInter_empty {α : Type u_1} :
= Set.univ
@[simp]
theorem Set.sUnion_singleton {α : Type u_1} (s : Set α) :
⋃₀ {s} = s
@[simp]
theorem Set.sInter_singleton {α : Type u_1} (s : Set α) :
⋂₀ {s} = s
@[simp]
theorem Set.sUnion_eq_empty {α : Type u_1} {S : Set (Set α)} :
⋃₀ S = sS, s =
@[simp]
theorem Set.sInter_eq_univ {α : Type u_1} {S : Set (Set α)} :
⋂₀ S = Set.univ sS, s = Set.univ
theorem Set.subset_powerset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} :
theorem Set.sUnion_powerset_gc {α : Type u_1} :
GaloisConnection (fun (x : Set (Set α)) => ⋃₀ x) fun (x : Set α) => 𝒫 x

⋃₀ and 𝒫 form a Galois connection.

def Set.sUnion_powerset_gi {α : Type u_1} :
GaloisInsertion (fun (x : Set (Set α)) => ⋃₀ x) fun (x : Set α) => 𝒫 x

⋃₀ and 𝒫 form a Galois insertion.

Equations
• Set.sUnion_powerset_gi = gi_sSup_Iic
Instances For
theorem Set.sUnion_mem_empty_univ {α : Type u_1} {S : Set (Set α)} (h : S {, Set.univ}) :
⋃₀ S {, Set.univ}

If all sets in a collection are either ∅ or Set.univ, then so is their union.

@[simp]
theorem Set.nonempty_sUnion {α : Type u_1} {S : Set (Set α)} :
(⋃₀ S).Nonempty sS, s.Nonempty
theorem Set.Nonempty.of_sUnion {α : Type u_1} {s : Set (Set α)} (h : (⋃₀ s).Nonempty) :
s.Nonempty
theorem Set.Nonempty.of_sUnion_eq_univ {α : Type u_1} [] {s : Set (Set α)} (h : ⋃₀ s = Set.univ) :
s.Nonempty
theorem Set.sUnion_union {α : Type u_1} (S : Set (Set α)) (T : Set (Set α)) :
theorem Set.sInter_union {α : Type u_1} (S : Set (Set α)) (T : Set (Set α)) :
@[simp]
theorem Set.sUnion_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) :
@[simp]
theorem Set.sInter_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) :
@[simp]
theorem Set.sUnion_diff_singleton_empty {α : Type u_1} (s : Set (Set α)) :
⋃₀ (s \ {}) = ⋃₀ s
@[simp]
theorem Set.sInter_diff_singleton_univ {α : Type u_1} (s : Set (Set α)) :
⋂₀ (s \ {Set.univ}) = ⋂₀ s
theorem Set.sUnion_pair {α : Type u_1} (s : Set α) (t : Set α) :
⋃₀ {s, t} = s t
theorem Set.sInter_pair {α : Type u_1} (s : Set α) (t : Set α) :
⋂₀ {s, t} = s t
@[simp]
theorem Set.sUnion_image {α : Type u_1} {β : Type u_2} (f : αSet β) (s : Set α) :
⋃₀ (f '' s) = xs, f x
@[simp]
theorem Set.sInter_image {α : Type u_1} {β : Type u_2} (f : αSet β) (s : Set α) :
⋂₀ (f '' s) = xs, f x
@[simp]
theorem Set.sUnion_range {β : Type u_2} {ι : Sort u_4} (f : ιSet β) :
= ⋃ (x : ι), f x
@[simp]
theorem Set.sInter_range {β : Type u_2} {ι : Sort u_4} (f : ιSet β) :
= ⋂ (x : ι), f x
theorem Set.iUnion_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {f : ιSet α} :
⋃ (i : ι), f i = Set.univ ∀ (x : α), ∃ (i : ι), x f i
theorem Set.iUnion₂_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} :
⋃ (i : ι), ⋃ (j : κ i), s i j = Set.univ ∀ (a : α), ∃ (i : ι) (j : κ i), a s i j
theorem Set.sUnion_eq_univ_iff {α : Type u_1} {c : Set (Set α)} :
⋃₀ c = Set.univ ∀ (a : α), bc, a b
theorem Set.iInter_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ιSet α} :
⋂ (i : ι), f i = ∀ (x : α), ∃ (i : ι), xf i
theorem Set.iInter₂_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} :
⋂ (i : ι), ⋂ (j : κ i), s i j = ∀ (a : α), ∃ (i : ι) (j : κ i), as i j
theorem Set.sInter_eq_empty_iff {α : Type u_1} {c : Set (Set α)} :
⋂₀ c = ∀ (a : α), bc, ab
@[simp]
theorem Set.nonempty_iInter {α : Type u_1} {ι : Sort u_4} {f : ιSet α} :
(⋂ (i : ι), f i).Nonempty ∃ (x : α), ∀ (i : ι), x f i
theorem Set.nonempty_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} :
(⋂ (i : ι), ⋂ (j : κ i), s i j).Nonempty ∃ (a : α), ∀ (i : ι) (j : κ i), a s i j
@[simp]
theorem Set.nonempty_sInter {α : Type u_1} {c : Set (Set α)} :
(⋂₀ c).Nonempty ∃ (a : α), bc, a b
theorem Set.compl_sUnion {α : Type u_1} (S : Set (Set α)) :
(⋃₀ S) = ⋂₀ (compl '' S)
theorem Set.sUnion_eq_compl_sInter_compl {α : Type u_1} (S : Set (Set α)) :
⋃₀ S = (⋂₀ (compl '' S))
theorem Set.compl_sInter {α : Type u_1} (S : Set (Set α)) :
(⋂₀ S) = ⋃₀ (compl '' S)
theorem Set.sInter_eq_compl_sUnion_compl {α : Type u_1} (S : Set (Set α)) :
⋂₀ S = (⋃₀ (compl '' S))
theorem Set.inter_empty_of_inter_sUnion_empty {α : Type u_1} {s : Set α} {t : Set α} {S : Set (Set α)} (hs : t S) (h : s ⋃₀ S = ) :
s t =
theorem Set.range_sigma_eq_iUnion_range {α : Type u_1} {β : Type u_2} {γ : αType u_11} (f : β) :
= ⋃ (a : α), Set.range fun (b : γ a) => f a, b
theorem Set.iUnion_eq_range_sigma {α : Type u_1} {β : Type u_2} (s : αSet β) :
⋃ (i : α), s i = Set.range fun (a : (i : α) × (s i)) => a.snd
theorem Set.iUnion_eq_range_psigma {β : Type u_2} {ι : Sort u_4} (s : ιSet β) :
⋃ (i : ι), s i = Set.range fun (a : (i : ι) ×' (s i)) => a.snd
theorem Set.iUnion_image_preimage_sigma_mk_eq_self {ι : Type u_11} {σ : ιType u_12} (s : Set (Sigma σ)) :
⋃ (i : ι), '' ( ⁻¹' s) = s
theorem Set.Sigma.univ {α : Type u_1} (X : αType u_11) :
Set.univ = ⋃ (a : α),
theorem Set.sUnion_mono {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S T) :

Alias of Set.sUnion_subset_sUnion.

theorem Set.sInter_mono {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S T) :

Alias of Set.sInter_subset_sInter.

theorem Set.iUnion_subset_iUnion_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : Set α} (h : ιι₂) :
⋃ (x : ι), s ⋃ (x : ι₂), s
@[simp]
theorem Set.iUnion_singleton_eq_range {α : Type u_11} {β : Type u_12} (f : αβ) :
⋃ (x : α), {f x} =
theorem Set.iUnion_of_singleton (α : Type u_11) :
⋃ (x : α), {x} = Set.univ
theorem Set.iUnion_of_singleton_coe {α : Type u_1} (s : Set α) :
⋃ (i : s), {i} = s
theorem Set.sUnion_eq_biUnion {α : Type u_1} {s : Set (Set α)} :
⋃₀ s = is, i
theorem Set.sInter_eq_biInter {α : Type u_1} {s : Set (Set α)} :
⋂₀ s = is, i
theorem Set.sUnion_eq_iUnion {α : Type u_1} {s : Set (Set α)} :
⋃₀ s = ⋃ (i : s), i
theorem Set.sInter_eq_iInter {α : Type u_1} {s : Set (Set α)} :
⋂₀ s = ⋂ (i : s), i
@[simp]
theorem Set.iUnion_of_empty {α : Type u_1} {ι : Sort u_4} [] (s : ιSet α) :
⋃ (i : ι), s i =
@[simp]
theorem Set.iInter_of_empty {α : Type u_1} {ι : Sort u_4} [] (s : ιSet α) :
⋂ (i : ι), s i = Set.univ
theorem Set.union_eq_iUnion {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :
s₁ s₂ = ⋃ (b : Bool), bif b then s₁ else s₂
theorem Set.inter_eq_iInter {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :
s₁ s₂ = ⋂ (b : Bool), bif b then s₁ else s₂
theorem Set.sInter_union_sInter {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} :
⋂₀ S ⋂₀ T = pS ×ˢ T, p.1 p.2
theorem Set.sUnion_inter_sUnion {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} :
⋃₀ s ⋃₀ t = ps ×ˢ t, p.1 p.2
theorem Set.biUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ιSet α) (t : αSet β) :
x⋃ (i : ι), s i, t x = ⋃ (i : ι), xs i, t x
theorem Set.biInter_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ιSet α) (t : αSet β) :
x⋃ (i : ι), s i, t x = ⋂ (i : ι), xs i, t x
theorem Set.sUnion_iUnion {α : Type u_1} {ι : Sort u_4} (s : ιSet (Set α)) :
⋃₀ ⋃ (i : ι), s i = ⋃ (i : ι), ⋃₀ s i
theorem Set.sInter_iUnion {α : Type u_1} {ι : Sort u_4} (s : ιSet (Set α)) :
⋂₀ ⋃ (i : ι), s i = ⋂ (i : ι), ⋂₀ s i
theorem Set.iUnion_range_eq_sUnion {α : Type u_11} {β : Type u_12} (C : Set (Set α)) {f : (s : C) → βs} (hf : ∀ (s : C), Function.Surjective (f s)) :
(⋃ (y : β), Set.range fun (s : C) => (f s y)) = ⋃₀ C
theorem Set.iUnion_range_eq_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (C : ιSet α) {f : (x : ι) → β(C x)} (hf : ∀ (x : ι), Function.Surjective (f x)) :
(⋃ (y : β), Set.range fun (x : ι) => (f x y)) = ⋃ (x : ι), C x
theorem Set.union_distrib_iInter_left {α : Type u_1} {ι : Sort u_4} (s : ιSet α) (t : Set α) :
t ⋂ (i : ι), s i = ⋂ (i : ι), t s i
theorem Set.union_distrib_iInter₂_left {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : Set α) (t : (i : ι) → κ iSet α) :
s ⋂ (i : ι), ⋂ (j : κ i), t i j = ⋂ (i : ι), ⋂ (j : κ i), s t i j
theorem Set.union_distrib_iInter_right {α : Type u_1} {ι : Sort u_4} (s : ιSet α) (t : Set α) :
(⋂ (i : ι), s i) t = ⋂ (i : ι), s i t
theorem Set.union_distrib_iInter₂_right {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} (s : (i : ι) → κ iSet α) (t : Set α) :
(⋂ (i : ι), ⋂ (j : κ i), s i j) t = ⋂ (i : ι), ⋂ (j : κ i), s i j t

### Lemmas about Set.MapsTo#

Porting note: some lemmas in this section were upgraded from implications to iffs.

@[simp]
theorem Set.mapsTo_sUnion {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : αβ} :
Set.MapsTo f (⋃₀ S) t sS, Set.MapsTo f s t
@[simp]
theorem Set.mapsTo_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} {t : Set β} {f : αβ} :
Set.MapsTo f (⋃ (i : ι), s i) t ∀ (i : ι), Set.MapsTo f (s i) t
theorem Set.mapsTo_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : Set β} {f : αβ} :
Set.MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) t ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t
theorem Set.mapsTo_iUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.MapsTo f (s i) (t i)) :
Set.MapsTo f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem Set.mapsTo_iUnion₂_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) :
Set.MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)
@[simp]
theorem Set.mapsTo_sInter {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : αβ} :
Set.MapsTo f s (⋂₀ T) tT, Set.MapsTo f s t
@[simp]
theorem Set.mapsTo_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ιSet β} {f : αβ} :
Set.MapsTo f s (⋂ (i : ι), t i) ∀ (i : ι), Set.MapsTo f s (t i)
theorem Set.mapsTo_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet β} {f : αβ} :
Set.MapsTo f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)
theorem Set.mapsTo_iInter_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.MapsTo f (s i) (t i)) :
Set.MapsTo f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
theorem Set.mapsTo_iInter₂_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) :
Set.MapsTo f (⋂ (i : ι), ⋂ (j : κ i), s i j) (⋂ (i : ι), ⋂ (j : κ i), t i j)
theorem Set.image_iInter_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ιSet α) (f : αβ) :
f '' ⋂ (i : ι), s i ⋂ (i : ι), f '' s i
theorem Set.image_iInter₂_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} (s : (i : ι) → κ iSet α) (f : αβ) :
f '' ⋂ (i : ι), ⋂ (j : κ i), s i j ⋂ (i : ι), ⋂ (j : κ i), f '' s i j
theorem Set.image_sInter_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (f : αβ) :
f '' ⋂₀ S sS, f '' s

### restrictPreimage#

theorem Set.injective_iff_injective_of_iUnion_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} {U : ιSet β} (hU : = Set.univ) :
∀ (i : ι), Function.Injective ((U i).restrictPreimage f)
theorem Set.surjective_iff_surjective_of_iUnion_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} {U : ιSet β} (hU : = Set.univ) :
∀ (i : ι), Function.Surjective ((U i).restrictPreimage f)
theorem Set.bijective_iff_bijective_of_iUnion_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} {U : ιSet β} (hU : = Set.univ) :
∀ (i : ι), Function.Bijective ((U i).restrictPreimage f)

### InjOn#

theorem Set.InjOn.image_iInter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {s : ιSet α} {f : αβ} (h : Set.InjOn f (⋃ (i : ι), s i)) :
f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
theorem Set.InjOn.image_biInter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {p : ιProp} {s : (i : ι) → p iSet α} (hp : ∃ (i : ι), p i) {f : αβ} (h : Set.InjOn f (⋃ (i : ι), ⋃ (hi : p i), s i hi)) :
f '' ⋂ (i : ι), ⋂ (hi : p i), s i hi = ⋂ (i : ι), ⋂ (hi : p i), f '' s i hi
theorem Set.image_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} (hf : ) (s : ιSet α) :
f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
theorem Set.image_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {f : αβ} (hf : ) (s : (i : ι) → κ iSet α) :
f '' ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), f '' s i j
theorem Set.inj_on_iUnion_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} (hs : Directed (fun (x1 x2 : Set α) => x1 x2) s) {f : αβ} (hf : ∀ (i : ι), Set.InjOn f (s i)) :
Set.InjOn f (⋃ (i : ι), s i)

### SurjOn#

theorem Set.surjOn_sUnion {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : αβ} (H : tT, Set.SurjOn f s t) :
theorem Set.surjOn_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f s (t i)) :
Set.SurjOn f s (⋃ (i : ι), t i)
theorem Set.surjOn_iUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f (s i) (t i)) :
Set.SurjOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem Set.surjOn_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.SurjOn f s (t i j)) :
Set.SurjOn f s (⋃ (i : ι), ⋃ (j : κ i), t i j)
theorem Set.surjOn_iUnion₂_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.SurjOn f (s i j) (t i j)) :
Set.SurjOn f (⋃ (i : ι), ⋃ (j : κ i), s i j) (⋃ (i : ι), ⋃ (j : κ i), t i j)
theorem Set.surjOn_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {s : ιSet α} {t : Set β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f (s i) t) (Hinj : Set.InjOn f (⋃ (i : ι), s i)) :
Set.SurjOn f (⋂ (i : ι), s i) t
theorem Set.surjOn_iInter_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f (s i) (t i)) (Hinj : Set.InjOn f (⋃ (i : ι), s i)) :
Set.SurjOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

### BijOn#

theorem Set.bijOn_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.BijOn f (s i) (t i)) (Hinj : Set.InjOn f (⋃ (i : ι), s i)) :
Set.BijOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem Set.bijOn_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [hi : ] {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.BijOn f (s i) (t i)) (Hinj : Set.InjOn f (⋃ (i : ι), s i)) :
Set.BijOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
theorem Set.bijOn_iUnion_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} (hs : Directed (fun (x1 x2 : Set α) => x1 x2) s) {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.BijOn f (s i) (t i)) :
Set.BijOn f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem Set.bijOn_iInter_of_directed {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] {s : ιSet α} (hs : Directed (fun (x1 x2 : Set α) => x1 x2) s) {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.BijOn f (s i) (t i)) :
Set.BijOn f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

### image, preimage#

theorem Set.image_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} {s : ιSet α} :
f '' ⋃ (i : ι), s i = ⋃ (i : ι), f '' s i
theorem Set.image_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} (f : αβ) (s : (i : ι) → κ iSet α) :
f '' ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), f '' s i j
theorem Set.univ_subtype {α : Type u_1} {p : αProp} :
Set.univ = ⋃ (x : α), ⋃ (h : p x), {x, h}
theorem Set.range_eq_iUnion {α : Type u_1} {ι : Sort u_11} (f : ια) :
= ⋃ (i : ι), {f i}
theorem Set.image_eq_iUnion {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
f '' s = is, {f i}
theorem Set.biUnion_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ια} {g : αSet β} :
x, g x = ⋃ (y : ι), g (f y)
@[simp]
theorem Set.iUnion_iUnion_eq' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ια} {g : αSet β} :
⋃ (x : α), ⋃ (y : ι), ⋃ (_ : f y = x), g x = ⋃ (y : ι), g (f y)
theorem Set.biInter_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ια} {g : αSet β} :
x, g x = ⋂ (y : ι), g (f y)
@[simp]
theorem Set.iInter_iInter_eq' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ια} {g : αSet β} :
⋂ (x : α), ⋂ (y : ι), ⋂ (_ : f y = x), g x = ⋂ (y : ι), g (f y)
theorem Set.biUnion_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γα} {g : αSet β} :
xf '' s, g x = ys, g (f y)
theorem Set.biInter_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γα} {g : αSet β} :
xf '' s, g x = ys, g (f y)
theorem Set.monotone_preimage {α : Type u_1} {β : Type u_2} {f : αβ} :
@[simp]
theorem Set.preimage_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} {s : ιSet β} :
f ⁻¹' ⋃ (i : ι), s i = ⋃ (i : ι), f ⁻¹' s i
theorem Set.preimage_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {f : αβ} {s : (i : ι) → κ iSet β} :
f ⁻¹' ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), f ⁻¹' s i j
theorem Set.image_sUnion {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set (Set α)} :
f '' ⋃₀ s = ⋃₀ ( '' s)
@[simp]
theorem Set.preimage_sUnion {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set (Set β)} :
f ⁻¹' ⋃₀ s = ts, f ⁻¹' t
theorem Set.preimage_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : αβ} {s : ιSet β} :
f ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), f ⁻¹' s i
theorem Set.preimage_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {f : αβ} {s : (i : ι) → κ iSet β} :
f ⁻¹' ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), f ⁻¹' s i j
@[simp]
theorem Set.preimage_sInter {α : Type u_1} {β : Type u_2} {f : αβ} {s : Set (Set β)} :
f ⁻¹' ⋂₀ s = ts, f ⁻¹' t
@[simp]
theorem Set.biUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
ys, f ⁻¹' {y} = f ⁻¹' s
theorem Set.biUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : αβ) :
y, f ⁻¹' {y} = Set.univ
theorem Set.prod_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ιSet β} :
s ×ˢ ⋃ (i : ι), t i = ⋃ (i : ι), s ×ˢ t i
theorem Set.prod_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet β} :
s ×ˢ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s ×ˢ t i j
theorem Set.prod_sUnion {α : Type u_1} {β : Type u_2} {s : Set α} {C : Set (Set β)} :
s ×ˢ ⋃₀ C = ⋃₀ ((fun (t : Set β) => s ×ˢ t) '' C)
theorem Set.iUnion_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ιSet α} {t : Set β} :
(⋃ (i : ι), s i) ×ˢ t = ⋃ (i : ι), s i ×ˢ t
theorem Set.iUnion₂_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : Set β} :
(⋃ (i : ι), ⋃ (j : κ i), s i j) ×ˢ t = ⋃ (i : ι), ⋃ (j : κ i), s i j ×ˢ t
theorem Set.sUnion_prod_const {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {t : Set β} :
⋃₀ C ×ˢ t = ⋃₀ ((fun (s : Set α) => s ×ˢ t) '' C)
theorem Set.iUnion_prod {ι : Type u_11} {ι' : Type u_12} {α : Type u_13} {β : Type u_14} (s : ιSet α) (t : ι'Set β) :
⋃ (x : ι × ι'), s x.1 ×ˢ t x.2 = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i
theorem Set.iUnion_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γSet α) :
⋃ (x : β × γ), f x = ⋃ (i : β), ⋃ (j : γ), f (i, j)

Analogue of iSup_prod for sets.

theorem Set.iUnion_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {s : αSet β} {t : αSet γ} (hs : ) (ht : ) :
⋃ (x : α), s x ×ˢ t x = (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
theorem Set.sInter_prod_sInter_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (T : Set (Set β)) :
⋂₀ S ×ˢ ⋂₀ T rS ×ˢ T, r.1 ×ˢ r.2
theorem Set.sInter_prod_sInter {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempty) (hT : T.Nonempty) :
⋂₀ S ×ˢ ⋂₀ T = rS ×ˢ T, r.1 ×ˢ r.2
theorem Set.sInter_prod {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) :
⋂₀ S ×ˢ t = sS, s ×ˢ t
theorem Set.prod_sInter {α : Type u_1} {β : Type u_2} {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) :
s ×ˢ ⋂₀ T = tT, s ×ˢ t
theorem Set.prod_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ιSet β} [hι : ] :
s ×ˢ ⋂ (i : ι), t i = ⋂ (i : ι), s ×ˢ t i
theorem Set.image2_eq_iUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (s : Set α) (t : Set β) :
Set.image2 f s t = is, jt, {f i j}

The Set.image2 version of Set.image_eq_iUnion

theorem Set.iUnion_image_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) {s : Set α} {t : Set β} :
as, f a '' t = Set.image2 f s t
theorem Set.iUnion_image_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) {s : Set α} {t : Set β} :
bt, (fun (x : α) => f x b) '' s = Set.image2 f s t
theorem Set.image2_iUnion_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : ιSet α) (t : Set β) :
Set.image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), Set.image2 f (s i) t
theorem Set.image2_iUnion_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : Set α) (t : ιSet β) :
Set.image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), Set.image2 f s (t i)
theorem Set.image2_iUnion₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_7} (f : αβγ) (s : (i : ι) → κ iSet α) (t : Set β) :
Set.image2 f (⋃ (i : ι), ⋃ (j : κ i), s i j) t = ⋃ (i : ι), ⋃ (j : κ i), Set.image2 f (s i j) t
theorem Set.image2_iUnion₂_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_7} (f : αβγ) (s : Set α) (t : (i : ι) → κ iSet β) :
Set.image2 f s (⋃ (i : ι), ⋃ (j : κ i), t i j) = ⋃ (i : ι), ⋃ (j : κ i), Set.image2 f s (t i j)
theorem Set.image2_iInter_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : ιSet α) (t : Set β) :
Set.image2 f (⋂ (i : ι), s i) t ⋂ (i : ι), Set.image2 f (s i) t
theorem Set.image2_iInter_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : Set α) (t : ιSet β) :
Set.image2 f s (⋂ (i : ι), t i) ⋂ (i : ι), Set.image2 f s (t i)
theorem Set.image2_iInter₂_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_7} (f : αβγ) (s : (i : ι) → κ iSet α) (t : Set β) :
Set.image2 f (⋂ (i : ι), ⋂ (j : κ i), s i j) t ⋂ (i : ι), ⋂ (j : κ i), Set.image2 f (s i j) t
theorem Set.image2_iInter₂_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_7} (f : αβγ) (s : Set α) (t : (i : ι) → κ iSet β) :
Set.image2 f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ⋂ (i : ι), ⋂ (j : κ i), Set.image2 f s (t i j)
theorem Set.prod_eq_biUnion_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
s ×ˢ t = as, (fun (b : β) => (a, b)) '' t
theorem Set.prod_eq_biUnion_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
s ×ˢ t = bt, (fun (a : α) => (a, b)) '' s
theorem Set.seq_def {α : Type u_1} {β : Type u_2} {s : Set (αβ)} {t : Set α} :
s.seq t = fs, f '' t
theorem Set.seq_subset {α : Type u_1} {β : Type u_2} {s : Set (αβ)} {t : Set α} {u : Set β} :
s.seq t u fs, at, f a u
theorem Set.seq_mono {α : Type u_1} {β : Type u_2} {s₀ : Set (αβ)} {s₁ : Set (αβ)} {t₀ : Set α} {t₁ : Set α} (hs : s₀ s₁) (ht : t₀ t₁) :
s₀.seq t₀ s₁.seq t₁
theorem Set.singleton_seq {α : Type u_1} {β : Type u_2} {f : αβ} {t : Set α} :
{f}.seq t = f '' t
theorem Set.seq_singleton {α : Type u_1} {β : Type u_2} {s : Set (αβ)} {a : α} :
s.seq {a} = (fun (f : αβ) => f a) '' s
theorem Set.seq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set (βγ)} {t : Set (αβ)} {u : Set α} :
s.seq (t.seq u) = (((fun (x1 : βγ) (x2 : αβ) => x1 x2) '' s).seq t).seq u
theorem Set.image_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βγ} {s : Set (αβ)} {t : Set α} :
f '' s.seq t = ((fun (x : αβ) => f x) '' s).seq t
theorem Set.prod_eq_seq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
s ×ˢ t = (Prod.mk '' s).seq t
theorem Set.prod_image_seq_comm {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
(Prod.mk '' s).seq t = ((fun (b : β) (a : α) => (a, b)) '' t).seq s
theorem Set.image2_eq_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (s : Set α) (t : Set β) :
Set.image2 f s t = (f '' s).seq t
theorem Set.pi_def {α : Type u_1} {π : αType u_11} (i : Set α) (s : (a : α) → Set (π a)) :
i.pi s = ai, ⁻¹' s a
theorem Set.univ_pi_eq_iInter {α : Type u_1} {π : αType u_11} (t : (i : α) → Set (π i)) :
Set.univ.pi t = ⋂ (i : α), ⁻¹' t i
theorem Set.pi_diff_pi_subset {α : Type u_1} {π : αType u_11} (i : Set α) (s : (a : α) → Set (π a)) (t : (a : α) → Set (π a)) :
i.pi s \ i.pi t ai, ⁻¹' (s a \ t a)
theorem Set.iUnion_univ_pi {α : Type u_1} {π : αType u_11} {ι : αType u_12} (t : (a : α) → ι aSet (π a)) :
(⋃ (x : (a : α) → ι a), Set.univ.pi fun (a : α) => t a (x a)) = Set.univ.pi fun (a : α) => ⋃ (j : ι a), t a j
theorem Set.directedOn_iUnion {α : Type u_1} {ι : Sort u_4} {r : ααProp} {f : ιSet α} (hd : Directed (fun (x1 x2 : Set α) => x1 x2) f) (h : ∀ (x : ι), DirectedOn r (f x)) :
DirectedOn r (⋃ (x : ι), f x)
@[deprecated Set.directedOn_iUnion]
theorem Set.directed_on_iUnion {α : Type u_1} {ι : Sort u_4} {r : ααProp} {f : ιSet α} (hd : Directed (fun (x1 x2 : Set α) => x1 x2) f) (h : ∀ (x : ι), DirectedOn r (f x)) :
DirectedOn r (⋃ (x : ι), f x)

Alias of Set.directedOn_iUnion.

theorem Set.directedOn_sUnion {α : Type u_1} {r : ααProp} {S : Set (Set α)} (hd : DirectedOn (fun (x1 x2 : Set α) => x1 x2) S) (h : xS, ) :
theorem Function.Surjective.iUnion_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ιι₂} (hf : ) (g : ι₂Set α) :
⋃ (x : ι), g (f x) = ⋃ (y : ι₂), g y
theorem Function.Surjective.iInter_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ιι₂} (hf : ) (g : ι₂Set α) :
⋂ (x : ι), g (f x) = ⋂ (y : ι₂), g y

### Disjoint sets #

@[simp]
theorem Set.disjoint_iUnion_left {α : Type u_1} {t : Set α} {ι : Sort u_11} {s : ιSet α} :
Disjoint (⋃ (i : ι), s i) t ∀ (i : ι), Disjoint (s i) t
@[simp]
theorem Set.disjoint_iUnion_right {α : Type u_1} {t : Set α} {ι : Sort u_11} {s : ιSet α} :
Disjoint t (⋃ (i : ι), s i) ∀ (i : ι), Disjoint t (s i)
theorem Set.disjoint_iUnion₂_left {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : (i : ι) → κ iSet α} {t : Set α} :
Disjoint (⋃ (i : ι), ⋃ (j : κ i), s i j) t ∀ (i : ι) (j : κ i), Disjoint (s i j) t
theorem Set.disjoint_iUnion₂_right {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} {s : Set α} {t : (i : ι) → κ iSet α} :
Disjoint s (⋃ (i : ι), ⋃ (j : κ i), t i j) ∀ (i : ι) (j : κ i), Disjoint s (t i j)
@[simp]
theorem Set.disjoint_sUnion_left {α : Type u_1} {S : Set (Set α)} {t : Set α} :
Disjoint (⋃₀ S) t sS, Disjoint s t
@[simp]
theorem Set.disjoint_sUnion_right {α : Type u_1} {s : Set α} {S : Set (Set α)} :
Disjoint s (⋃₀ S) tS, Disjoint s t
theorem Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ {α : Type u_1} {ι : Type u_11} {Es : ιSet α} (Es_union : ⋃ (i : ι), Es i = Set.univ) (Es_disj : Pairwise fun (i j : ι) => Disjoint (Es i) (Es j)) (I : Set ι) :
(⋃ iI, Es i) = iI, Es i

### Intervals #

theorem Set.nonempty_iInter_Iic_iff {α : Type u_1} {ι : Sort u_4} [] {f : ια} :
(⋂ (i : ι), Set.Iic (f i)).Nonempty
theorem Set.nonempty_iInter_Ici_iff {α : Type u_1} {ι : Sort u_4} [] {f : ια} :
(⋂ (i : ι), Set.Ici (f i)).Nonempty
theorem Set.Ici_iSup {α : Type u_1} {ι : Sort u_4} [] (f : ια) :
Set.Ici (⨆ (i : ι), f i) = ⋂ (i : ι), Set.Ici (f i)
theorem Set.Iic_iInf {α : Type u_1} {ι : Sort u_4} [] (f : ια) :
Set.Iic (⨅ (i : ι), f i) = ⋂ (i : ι), Set.Iic (f i)
theorem Set.Ici_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} [] (f : (i : ι) → κ iα) :
Set.Ici (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), Set.Ici (f i j)
theorem Set.Iic_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_7} [] (f : (i : ι) → κ iα) :
Set.Iic (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), Set.Iic (f i j)
theorem Set.Ici_sSup {α : Type u_1} [] (s : Set α) :
Set.Ici (sSup s) = as,
theorem Set.Iic_sInf {α : Type u_1} [] (s : Set α) :
Set.Iic (sInf s) = as,
theorem Set.biUnion_diff_biUnion_subset {α : Type u_1} {β : Type u_2} (t : αSet β) (s₁ : Set α) (s₂ : Set α) :
(⋃ xs₁, t x) \ xs₂, t x xs₁ \ s₂, t x
def Set.sigmaToiUnion {α : Type u_1} {β : Type u_2} (t : αSet β) (x : (i : α) × (t i)) :
(⋃ (i : α), t i)

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.

Equations
• = x.snd,
Instances For
theorem Set.sigmaToiUnion_surjective {α : Type u_1} {β : Type u_2} (t : αSet β) :
theorem Set.sigmaToiUnion_injective {α : Type u_1} {β : Type u_2} (t : αSet β) (h : Pairwise fun (i j : α) => Disjoint (t i) (t j)) :
theorem Set.sigmaToiUnion_bijective {α : Type u_1} {β : Type u_2} (t : αSet β) (h : Pairwise fun (i j : α) => Disjoint (t i) (t j)) :
noncomputable def Set.sigmaEquiv {α : Type u_1} {β : Type u_2} (s : αSet β) (hs : ∀ (b : β), ∃! i : α, b s i) :
(i : α) × (s i) β

Equivalence from the disjoint union of a family of sets forming a partition of β, to β itself.

Equations
• = { toFun := fun (x : (i : α) × (s i)) => match x with | fst, b => b, invFun := fun (b : β) => ⟨, b, , left_inv := , right_inv := }
Instances For
noncomputable def Set.unionEqSigmaOfDisjoint {α : Type u_1} {β : Type u_2} {t : αSet β} (h : Pairwise fun (i j : α) => Disjoint (t i) (t j)) :
(⋃ (i : α), t i) (i : α) × (t i)

Equivalence between a disjoint union and a dependent sum.

Equations
• = .symm
Instances For
theorem Set.iUnion_ge_eq_iUnion_nat_add {α : Type u_1} (u : Set α) (n : ) :
⋃ (i : ), ⋃ (_ : i n), u i = ⋃ (i : ), u (i + n)
theorem Set.iInter_ge_eq_iInter_nat_add {α : Type u_1} (u : Set α) (n : ) :
⋂ (i : ), ⋂ (_ : i n), u i = ⋂ (i : ), u (i + n)
theorem Monotone.iUnion_nat_add {α : Type u_1} {f : Set α} (hf : ) (k : ) :
⋃ (n : ), f (n + k) = ⋃ (n : ), f n
theorem Antitone.iInter_nat_add {α : Type u_1} {f : Set α} (hf : ) (k : ) :
⋂ (n : ), f (n + k) = ⋂ (n : ), f n
theorem Set.iUnion_iInter_ge_nat_add {α : Type u_1} (f : Set α) (k : ) :
⋃ (n : ), ⋂ (i : ), ⋂ (_ : i n), f (i + k) = ⋃ (n : ), ⋂ (i : ), ⋂ (_ : i n), f i
theorem Set.union_iUnion_nat_succ {α : Type u_1} (u : Set α) :
u 0 ⋃ (i : ), u (i + 1) = ⋃ (i : ), u i
theorem Set.inter_iInter_nat_succ {α : Type u_1} (u : Set α) :
u 0 ⋂ (i : ), u (i + 1) = ⋂ (i : ), u i
theorem iSup_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] (s : ιSet α) (f : αβ) :
a⋃ (i : ι), s i, f a = ⨆ (i : ι), as i, f a
theorem iInf_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [] (s : ιSet α) (f : αβ) :
a⋃ (i : ι), s i, f a = ⨅ (i : ι), as i, f a
theorem sSup_iUnion {β : Type u_2} {ι : Sort u_4} [] (t : ιSet β) :
sSup (⋃ (i : ι), t i) = ⨆ (i : ι), sSup (t i)
theorem sSup_sUnion {β : Type u_2} [] (s : Set (Set β)) :
sSup (⋃₀ s) = ts, sSup t
theorem sInf_sUnion {β : Type u_2} [] (s : Set (Set β)) :
sInf (⋃₀ s) = ts, sInf t
theorem iSup_sUnion {α : Type u_1} {β : Type u_2} [] (S : Set (Set α)) (f : αβ) :
x⋃₀ S, f x = sS, xs, f x
theorem iInf_sUnion {α : Type u_1} {β : Type u_2} [] (S : Set (Set α)) (f : αβ) :
x⋃₀ S, f x = sS, xs, f x
theorem forall_sUnion {α : Type u_1} {S : Set (Set α)} {p : αProp} :
(∀ x⋃₀ S, p x) sS, xs, p x
theorem exists_sUnion {α : Type u_1} {S : Set (Set α)} {p : αProp} :
(∃ x⋃₀ S, p x) sS, xs, p x