Bounded and set-indexed unions and intersections

This file develops bounded indexed unions and intersections of sets, together with unions and intersections indexed by sets of sets. It relates biUnion and biInter to subtype-indexed families and relates sUnion and sInter to indexed families. It also contains results about products of families of sets, directed unions, and reindexing along surjective functions.

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 ∈ ⋃ x ∈ s, t x

A specialization of mem_iUnion₂.

theorem Set.mem_biInter {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) : y ∈ ⋂ x ∈ s, 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 ⊆ ⋃ x ∈ s, 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) : ⋂ x ∈ s, t x ⊆ t x

A specialization of iInter₂_subset.

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

theorem Set.biUnion_subset_biUnion_left {α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β} (h : s ⊆ s') : ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x

theorem Set.biInter_subset_biInter_left {α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β} (h : s' ⊆ s) : ⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x

theorem Set.biUnion_mono {α : Type u_1} {β : Type u_2} {s s' : Set α} {t t' : α → Set β} (hs : s' ⊆ s) (h : ∀ x ∈ s, t x ⊆ t' x) : ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x

theorem Set.biInter_mono {α : Type u_1} {β : Type u_2} {s s' : Set α} {t t' : α → Set β} (hs : s ⊆ s') (h : ∀ x ∈ s, t x ⊆ t' x) : ⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x

theorem Set.biUnion_eq_iUnion {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β) : ⋃ (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 ∈ s → Set β) : ⋂ (x : α), ⋂ (h : x ∈ s), t x h = ⋂ (x : ↑s), t ↑x ⋯

@[simp]

theorem Set.biUnion_const {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) (t : Set β) : ⋃ a ∈ s, t = t

@[simp]

theorem Set.biInter_const {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) (t : Set β) : ⋂ a ∈ s, t = t

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 = univ

theorem Set.biInter_univ {α : Type u_1} {β : Type u_2} (u : α → Set β) : ⋂ x ∈ univ, u x = ⋂ (x : α), u x

@[simp]

theorem Set.biUnion_self {α : Type u_1} (s : Set α) : ⋃ x ∈ s, s = s

@[simp]

theorem Set.iUnion_nonempty_self {α : Type u_1} (s : Set α) : ⋃ (_ : s.Nonempty), s = s

@[simp]

theorem Set.iInter_ne_univ_self {α : Type u_1} (s : Set α) : ⋂ (_ : s ≠ univ), 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 t : Set α) (u : α → Set β) : ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x

theorem Set.biInter_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β) : ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, 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_7} {α : Type u_8} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) : ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

theorem Set.inter_biInter {ι : Type u_7} {α : Type u_8} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) : ⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, 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 β) : ⋃ x ∈ 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 α) : ⋃ x ∈ s, {x} = s

theorem Set.biUnion_union {α : Type u_1} {β : Type u_2} (s t : Set α) (u : α → Set β) : ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x

@[simp]

theorem Set.iUnion_coe_set {α : Type u_7} {β : Type u_8} (s : Set α) (f : ↑s → Set β) : ⋃ (i : ↑s), f i = ⋃ (i : α), ⋃ (h : i ∈ s), f ⟨i, h⟩

@[simp]

theorem Set.iInter_coe_set {α : Type u_7} {β : Type u_8} (s : Set α) (f : ↑s → Set β) : ⋂ (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 β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, 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_6} (s : Set α) (t : (i : ι) → κ i → Set α) : 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_6} (s : (i : ι) → κ i → Set α) (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_6} (s : Set α) (t : (i : ι) → κ i → Set α) : 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_6} (s : (i : ι) → κ i → Set α) (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) : x ∈ ⋃₀ S

theorem Set.notMem_of_notMem_sUnion {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)} (hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t

theorem Set.sInter_subset_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t ∈ S) : ⋂₀ S ⊆ t

theorem Set.subset_sUnion_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t ∈ S) : t ⊆ ⋃₀ S

theorem Set.subset_sUnion_of_subset {α : Type u_1} {s : Set α} (t : Set (Set α)) (u : Set α) (h₁ : s ⊆ u) (h₂ : u ∈ t) : s ⊆ ⋃₀ t

theorem Set.sUnion_subset {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t' ⊆ t) : ⋃₀ S ⊆ 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) : ⋃₀ s ⊆ ⋃₀ (f '' s)

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) : ⋃₀ (f '' s) ⊆ ⋃₀ s

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') : t ⊆ ⋂₀ S

@[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 T : Set (Set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T

theorem Set.sInter_subset_sInter {α : Type u_1} {S T : Set (Set α)} (h : S ⊆ T) : ⋂₀ T ⊆ ⋂₀ S

@[simp]

theorem Set.sUnion_empty {α : Type u_1} : ⋃₀ ∅ = ∅

@[simp]

theorem Set.sInter_empty {α : Type u_1} : ⋂₀ ∅ = 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 = ∅ ↔ ∀ s ∈ S, s = ∅

@[simp]

theorem Set.sInter_eq_univ {α : Type u_1} {S : Set (Set α)} : ⋂₀ S = univ ↔ ∀ s ∈ S, s = univ

theorem Set.subset_powerset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} : s ⊆ 𝒫 t ↔ ⋃₀ s ⊆ t

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.sUnionPowersetGI {α : Type u_1} : GaloisInsertion (fun (x : Set (Set α)) => ⋃₀ x) fun (x : Set α) => 𝒫 x

⋃₀ and 𝒫 form a Galois insertion.

Equations

• Set.sUnionPowersetGI = giSSupIic

theorem Set.sUnion_mem_empty_univ {α : Type u_1} {S : Set (Set α)} (h : S ⊆ {∅, univ}) : ⋃₀ S ∈ {∅, 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 ↔ ∃ s ∈ S, 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} [Nonempty α] {s : Set (Set α)} (h : ⋃₀ s = univ) : s.Nonempty

theorem Set.sUnion_union {α : Type u_1} (S T : Set (Set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T

theorem Set.sInter_union {α : Type u_1} (S T : Set (Set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T

@[simp]

theorem Set.sUnion_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) : ⋃₀ insert s T = s ∪ ⋃₀ T

@[simp]

theorem Set.sInter_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) : ⋂₀ insert s T = s ∩ ⋂₀ T

@[simp]

theorem Set.sUnion_sdiff_singleton_empty {α : Type u_1} (s : Set (Set α)) : ⋃₀ (s \ {∅}) = ⋃₀ s

@[deprecated Set.sUnion_sdiff_singleton_empty (since := "2026-06-03")]

theorem Set.sUnion_diff_singleton_empty {α : Type u_1} (s : Set (Set α)) : ⋃₀ (s \ {∅}) = ⋃₀ s

Alias of Set.sUnion_sdiff_singleton_empty.

@[simp]

theorem Set.sInter_sdiff_singleton_univ {α : Type u_1} (s : Set (Set α)) : ⋂₀ (s \ {univ}) = ⋂₀ s

@[deprecated Set.sInter_sdiff_singleton_univ (since := "2026-06-03")]

theorem Set.sInter_diff_singleton_univ {α : Type u_1} (s : Set (Set α)) : ⋂₀ (s \ {univ}) = ⋂₀ s

Alias of Set.sInter_sdiff_singleton_univ.

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

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

@[simp]

theorem Set.sUnion_image {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α) : ⋃₀ (f '' s) = ⋃ a ∈ s, f a

@[simp]

theorem Set.sInter_image {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α) : ⋂₀ (f '' s) = ⋂ a ∈ s, f a

@[simp]

theorem Set.sUnion_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → Set γ) (s : Set α) (t : Set β) : ⋃₀ image2 f s t = ⋃ a ∈ s, ⋃ b ∈ t, f a b

@[simp]

theorem Set.sInter_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → Set γ) (s : Set α) (t : Set β) : ⋂₀ image2 f s t = ⋂ a ∈ s, ⋂ b ∈ t, f a b

@[simp]

theorem Set.sUnion_range {β : Type u_2} {ι : Sort u_4} (f : ι → Set β) : ⋃₀ range f = ⋃ (x : ι), f x

@[simp]

theorem Set.sInter_range {β : Type u_2} {ι : Sort u_4} (f : ι → Set β) : ⋂₀ range f = ⋂ (x : ι), f x

theorem Set.iUnion_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {f : ι → Set α} : ⋃ (i : ι), f i = univ ↔ ∀ (x : α), ∃ (i : ι), x ∈ f i

theorem Set.iUnion₂_eq_univ_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} {s : (i : ι) → κ i → Set α} : ⋃ (i : ι), ⋃ (j : κ i), s i j = univ ↔ ∀ (a : α), ∃ (i : ι) (j : κ i), a ∈ s i j

theorem Set.sUnion_eq_univ_iff {α : Type u_1} {c : Set (Set α)} : ⋃₀ c = univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b

theorem Set.iInter_eq_empty_of_eq_empty {α : Type u_1} {ι : Sort u_4} {i : ι} {f : ι → Set α} (h : f i = ∅) : ⋂ (j : ι), f j = ∅

theorem Set.iInter_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {f : ι → Set α} : ⋂ (i : ι), f i = ∅ ↔ ∀ (x : α), ∃ (i : ι), x ∉ f i

theorem Set.iInter₂_eq_empty_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} {s : (i : ι) → κ i → Set α} : ⋂ (i : ι), ⋂ (j : κ i), s i j = ∅ ↔ ∀ (a : α), ∃ (i : ι) (j : κ i), a ∉ s i j

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

@[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_6} {s : (i : ι) → κ i → Set α} : (⋂ (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 : α), ∀ b ∈ c, 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 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_7} (f : Sigma γ → β) : range f = ⋃ (a : α), range fun (b : γ a) => f ⟨a, b⟩

theorem Set.iUnion_eq_range_sigma {α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ (i : α), s i = 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 = range fun (a : (i : ι) ×' ↑(s i)) => ↑a.snd

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

theorem Set.Sigma.univ {α : Type u_1} (X : α → Type u_7) : Set.univ = ⋃ (a : α), range (Sigma.mk a)

theorem Set.sUnion_mono {α : Type u_1} {S T : Set (Set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T

Alias of Set.sUnion_subset_sUnion.

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

Alias of Set.sInter_subset_sInter.

theorem Set.iUnion_subset_iUnion_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} {s : Set α} (h : ι → ι₂) : ⋃ (x : ι), s ⊆ ⋃ (x : ι₂), s

@[simp]

theorem Set.iUnion_singleton_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) : ⋃ (x : α), {f x} = range f

theorem Set.iUnion_insert_eq_range_union_iUnion {β : Type u_2} {ι : Type u_7} (x : ι → β) (t : ι → Set β) : ⋃ (i : ι), insert (x i) (t i) = range x ∪ ⋃ (i : ι), t i

theorem Set.iUnion_of_singleton (α : Type u_7) : ⋃ (x : α), {x} = 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 = ⋃ i ∈ s, i

theorem Set.sInter_eq_biInter {α : Type u_1} {s : Set (Set α)} : ⋂₀ s = ⋂ i ∈ s, 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} [IsEmpty ι] (s : ι → Set α) : ⋃ (i : ι), s i = ∅

@[simp]

theorem Set.iInter_of_empty {α : Type u_1} {ι : Sort u_4} [IsEmpty ι] (s : ι → Set α) : ⋂ (i : ι), s i = univ

theorem Set.union_eq_iUnion {α : Type u_1} {s₁ s₂ : Set α} : s₁ ∪ s₂ = ⋃ (b : Bool), bif b then s₁ else s₂

theorem Set.inter_eq_iInter {α : Type u_1} {s₁ s₂ : Set α} : s₁ ∩ s₂ = ⋂ (b : Bool), bif b then s₁ else s₂

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

theorem Set.sUnion_inter_sUnion {α : Type u_1} {s t : Set (Set α)} : ⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ 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 : ι), ⋃ x ∈ s 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 : ι), ⋂ x ∈ s 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_7} {β : Type u_8} (C : Set (Set α)) {f : (s : ↑C) → β → ↑↑s} (hf : ∀ (s : ↑C), Function.Surjective (f s)) : (⋃ (y : β), 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 : β), range fun (x : ι) => ↑(f x y)) = ⋃ (x : ι), C x

theorem Set.iUnion_sumElim {α : Type u_1} {ι : Type u_7} {σ : Type u_8} (s : ι → Set α) (t : σ → Set α) : ⋃ (x : ι ⊕ σ), Sum.elim s t x = (⋃ (x : ι), s x) ∪ ⋃ (x : σ), t 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_6} (s : Set α) (t : (i : ι) → κ i → Set α) : 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_6} (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) ∪ t = ⋂ (i : ι), ⋂ (j : κ i), s i j ∪ t

theorem Set.biUnion_lt_eq_iUnion {α : Type u_1} {β : Type u_2} [LT α] [NoMaxOrder α] {s : α → Set β} : ⋃ (n : α), ⋃ (m : α), ⋃ (_ : m < n), s m = ⋃ (n : α), s n

theorem Set.biUnion_le_eq_iUnion {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} : ⋃ (n : α), ⋃ (m : α), ⋃ (_ : m ≤ n), s m = ⋃ (n : α), s n

theorem Set.biInter_lt_eq_iInter {α : Type u_1} {β : Type u_2} [LT α] [NoMaxOrder α] {s : α → Set β} : ⋂ (n : α), ⋂ (m : α), ⋂ (_ : m < n), s m = ⋂ (n : α), s n

theorem Set.biInter_le_eq_iInter {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} : ⋂ (n : α), ⋂ (m : α), ⋂ (_ : m ≤ n), s m = ⋂ (n : α), s n

theorem Set.biUnion_gt_eq_iUnion {α : Type u_1} {β : Type u_2} [LT α] [NoMinOrder α] {s : α → Set β} : ⋃ (n : α), ⋃ (m : α), ⋃ (_ : m > n), s m = ⋃ (n : α), s n

theorem Set.biUnion_ge_eq_iUnion {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} : ⋃ (n : α), ⋃ (m : α), ⋃ (_ : m ≥ n), s m = ⋃ (n : α), s n

theorem Set.biInter_gt_eq_iInf {α : Type u_1} {β : Type u_2} [LT α] [NoMinOrder α] {s : α → Set β} : ⋂ (n : α), ⋂ (m : α), ⋂ (_ : m > n), s m = ⋂ (n : α), s n

theorem Set.biInter_ge_eq_iInf {α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} : ⋂ (n : α), ⋂ (m : α), ⋂ (_ : m ≥ n), s m = ⋂ (n : α), s n

theorem Set.biUnion_le {α : Type u_1} {ι : Type u_7} [PartialOrder ι] (s : ι → Set α) (i : ι) : ⋃ (j : ι), ⋃ (_ : j ≤ i), s j = (⋃ (j : ι), ⋃ (_ : j < i), s j) ∪ s i

theorem Set.biInter_le {α : Type u_1} {ι : Type u_7} [PartialOrder ι] (s : ι → Set α) (i : ι) : ⋂ (j : ι), ⋂ (_ : j ≤ i), s j = (⋂ (j : ι), ⋂ (_ : j < i), s j) ∩ s i

theorem Set.biUnion_ge {α : Type u_1} {ι : Type u_7} [PartialOrder ι] (s : ι → Set α) (i : ι) : ⋃ (j : ι), ⋃ (_ : j ≥ i), s j = s i ∪ ⋃ (j : ι), ⋃ (_ : j > i), s j

theorem Set.biInter_ge {α : Type u_1} {ι : Type u_7} [PartialOrder ι] (s : ι → Set α) (i : ι) : ⋂ (j : ι), ⋂ (_ : j ≥ i), s j = s i ∩ ⋂ (j : ι), ⋂ (_ : j > i), s j

theorem Set.pi_def {α : Type u_1} {π : α → Type u_7} (i : Set α) (s : (a : α) → Set (π a)) : i.pi s = ⋂ a ∈ i, Function.eval a ⁻¹' s a

theorem Set.univ_pi_eq_iInter {α : Type u_1} {π : α → Type u_7} (t : (i : α) → Set (π i)) : univ.pi t = ⋂ (i : α), Function.eval i ⁻¹' t i

theorem Set.pi_sdiff_pi_subset {α : Type u_1} {π : α → Type u_7} (i : Set α) (s t : (a : α) → Set (π a)) : i.pi s \ i.pi t ⊆ ⋃ a ∈ i, Function.eval a ⁻¹' (s a \ t a)

@[deprecated Set.pi_sdiff_pi_subset (since := "2026-06-03")]

theorem Set.pi_diff_pi_subset {α : Type u_1} {π : α → Type u_7} (i : Set α) (s t : (a : α) → Set (π a)) : i.pi s \ i.pi t ⊆ ⋃ a ∈ i, Function.eval a ⁻¹' (s a \ t a)

Alias of Set.pi_sdiff_pi_subset.

theorem Set.iUnion_univ_pi {α : Type u_1} {π : α → Type u_7} {ι : α → Type u_8} (t : (a : α) → ι a → Set (π a)) : (⋃ (x : (a : α) → ι a), univ.pi fun (a : α) => t a (x a)) = univ.pi fun (a : α) => ⋃ (j : ι a), t a j

theorem Set.biUnion_univ_pi {α : Type u_1} {π : α → Type u_7} {ι : α → Type u_8} (s : (a : α) → Set (ι a)) (t : (a : α) → ι a → Set (π a)) : (⋃ x ∈ univ.pi s, univ.pi fun (a : α) => t a (x a)) = univ.pi fun (a : α) => ⋃ j ∈ s a, t a j

theorem Set.pi_iUnion_eq_iInter_pi {α : Type u_1} {π : α → Type u_7} {α' : Type u_8} (s : α' → Set α) (t : (a : α) → Set (π a)) : (⋃ (i : α'), s i).pi t = ⋂ (i : α'), (s i).pi t

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)

theorem Set.directedOn_sUnion {α : Type u_1} {r : α → α → Prop} {S : Set (Set α)} (hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) S) (h : ∀ x ∈ S, DirectedOn r x) : DirectedOn r (⋃₀ S)

theorem Function.Surjective.iUnion_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} {f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋃ (x : ι), g (f x) = ⋃ (y : ι₂), g y

theorem Function.Surjective.iInter_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} {f : ι → ι₂} (hf : Surjective f) (g : ι₂ → Set α) : ⋂ (x : ι), g (f x) = ⋂ (y : ι₂), g y

theorem Set.biUnion_sdiff_biUnion_subset {α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ s₂ : Set α) : (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x

@[deprecated Set.biUnion_sdiff_biUnion_subset (since := "2026-06-03")]

theorem Set.biUnion_diff_biUnion_subset {α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ s₂ : Set α) : (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x

Alias of Set.biUnion_sdiff_biUnion_subset.