Indexed unions and intersections of sets

This file develops the basic theory of indexed unions and intersections of sets. It includes membership and inclusion lemmas, congruence and monotonicity results, interaction with complements and Boolean operations, unions and intersections indexed by propositions, and reindexing results for sums and dependent sums.

In lemma names, iUnion₂ and iInter₂ refer to two nested indexed unions or intersections, while biUnion and biInter refer to the special case in which the inner index is a membership proof.

Basic membership lemmas

theorem Set.mem_iUnion₂ {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} {x : γ} {s : (i : ι) → κ i → Set γ} : 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 : ι) → κ i → Set γ} : 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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} {a : α} (h : ∀ (i : ι) (j : κ i), a ∈ s i j) : a ∈ ⋂ (i : ι), ⋂ (j : κ i), s i j

Union and intersection over an indexed family of sets

theorem Set.iUnion_congr_Prop {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = f₂ x) : iUnion f₁ = iUnion f₂

theorem Set.iInter_congr_Prop {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = f₂ x) : iInter f₁ = iInter f₂

theorem Set.iUnion_plift_up {α : Type u_1} {ι : Sort u_4} (f : PLift ι → Set α) : ⋃ (i : ι), f { down := i } = ⋃ (i : PLift ι), f i

theorem Set.iUnion_plift_down {α : Type u_1} {ι : Sort u_4} (f : ι → Set α) : ⋃ (i : PLift ι), f i.down = ⋃ (i : ι), f i

theorem Set.iInter_plift_up {α : Type u_1} {ι : Sort u_4} (f : PLift ι → Set α) : ⋂ (i : ι), f { down := i } = ⋂ (i : PLift ι), f i

theorem Set.iInter_plift_down {α : Type u_1} {ι : Sort u_4} (f : ι → Set α) : ⋂ (i : PLift ι), f i.down = ⋂ (i : ι), f i

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

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

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

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

theorem Set.exists_set_mem_of_union_eq_top {β : Type u_2} {ι : Type u_9} (t : Set ι) (s : ι → Set β) (w : ⋃ i ∈ t, s i = ⊤) (x : β) : ∃ i ∈ t, x ∈ s i

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

theorem Set.nonempty_of_nonempty_iUnion {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} (h_Union : (⋃ (i : ι), s i).Nonempty) : Nonempty ι

theorem Set.nonempty_of_nonempty_iUnion_eq_univ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} [Nonempty α] (h_Union : ⋃ (i : ι), s i = univ) : Nonempty ι

theorem Set.ofPred_exists {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop) : {x : β | ∃ (i : ι), p i x} = ⋃ (i : ι), {x : β | p i x}

@[deprecated Set.ofPred_exists (since := "2026-07-09")]

theorem Set.setOf_exists {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop) : {x : β | ∃ (i : ι), p i x} = ⋃ (i : ι), {x : β | p i x}

Alias of Set.ofPred_exists.

theorem Set.ofPred_forall {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop) : {x : β | ∀ (i : ι), p i x} = ⋂ (i : ι), {x : β | p i x}

@[deprecated Set.ofPred_forall (since := "2026-07-09")]

theorem Set.setOf_forall {β : Type u_2} {ι : Sort u_4} (p : ι → β → Prop) : {x : β | ∀ (i : ι), p i x} = ⋂ (i : ι), {x : β | p i x}

Alias of Set.ofPred_forall.

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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} : 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.iInter_subset_iUnion {α : Type u_1} {ι : Sort u_4} [Nonempty ι] {s : ι → Set α} : ⋂ (i : ι), s i ⊆ ⋃ (i : ι), s i

theorem Set.subset_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} (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 : ι) → κ i → Set α} (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_iUnion is 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_subset is 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 : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {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 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 t : ι → Set α} (h : ∀ (i : ι), s i ⊆ t i) : iUnion s ⊆ iUnion t

theorem Set.iUnion₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s t : (i : ι) → κ i → Set α} (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 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 t : ι → Set α} (h : ∀ (i : ι), s i ⊆ t i) : iInter s ⊆ iInter t

theorem Set.iInter₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s t : (i : ι) → κ i → Set α} (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_8} {s : (i : ι) → κ i → Set α} {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_8} {s : (i : ι) → κ i → Set α} {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_9) (s : ι → Set α) : ⋃ (i : ι), ⋃ (x : κ i), s i ⊆ ⋃ (i : ι), s i

theorem Set.iInter_subset_iInter₂ {α : Type u_1} {ι : Sort u_4} (κ : ι → Sort u_9) (s : ι → Set α) : ⋂ (i : ι), s i ⊆ ⋂ (i : ι), ⋂ (x : κ i), s i

theorem Set.iUnion_ofPred {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop) : ⋃ (i : ι), {x : α | P i x} = {x : α | ∃ (i : ι), P i x}

@[deprecated Set.iUnion_ofPred (since := "2026-07-09")]

theorem Set.iUnion_setOf {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop) : ⋃ (i : ι), {x : α | P i x} = {x : α | ∃ (i : ι), P i x}

Alias of Set.iUnion_ofPred.

theorem Set.iInter_ofPred {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop) : ⋂ (i : ι), {x : α | P i x} = {x : α | ∀ (i : ι), P i x}

@[deprecated Set.iInter_ofPred (since := "2026-07-09")]

theorem Set.iInter_setOf {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop) : ⋂ (i : ι), {x : α | P i x} = {x : α | ∀ (i : ι), P i x}

Alias of Set.iInter_ofPred.

theorem Set.forall_mem_iUnion {α : Type u_1} {ι : Sort u_4} {p : α → Prop} {f : ι → Set α} : (∀ x ∈ ⋃ (i : ι), f i, p x) ↔ ∀ (i : ι), ∀ x ∈ f i, p x

theorem Set.exists_mem_iUnion {α : Type u_1} {ι : Sort u_4} {p : α → Prop} {f : ι → Set α} : (∃ x ∈ ⋃ (i : ι), f i, p x) ↔ ∃ (i : ι), ∃ x ∈ f i, p x

theorem Set.forall_mem_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {p : α → Prop} {f : (i : ι) → κ i → Set α} : (∀ x ∈ ⋃ (i : ι), ⋃ (j : κ i), f i j, p x) ↔ ∀ (i : ι) (j : κ i), ∀ x ∈ f i j, p x

theorem Set.exists_mem_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {p : α → Prop} {f : (i : ι) → κ i → Set α} : (∃ x ∈ ⋃ (i : ι), ⋃ (j : κ i), f i j, p x) ↔ ∃ (i : ι) (j : κ i), ∃ x ∈ f i j, p x

theorem Set.forall_mem_biUnion {α : Type u_1} {ι : Sort u_4} {p : α → Prop} {f : ι → Set α} {q : ι → Prop} : (∀ x ∈ ⋃ (i : ι), ⋃ (_ : q i), f i, p x) ↔ ∀ (i : ι), q i → ∀ x ∈ f i, p x

theorem Set.exists_mem_biUnion {α : Type u_1} {ι : Sort u_4} {p : α → Prop} {f : ι → Set α} {q : ι → Prop} : (∃ x ∈ ⋃ (i : ι), ⋃ (_ : q i), f i, p x) ↔ ∃ (i : ι), q i ∧ ∃ x ∈ f i, p x

theorem Set.iUnion_congr_of_surjective {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Function.Surjective h) (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 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) : ⋂ (x : ι), f x = ⋂ (y : ι₂), g y

theorem Set.iUnion_congr {α : Type u_1} {ι : Sort u_4} {s 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 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 t : (i : ι) → κ i → Set α} (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 t : (i : ι) → κ i → Set α} (h : ∀ (i : ι) (j : κ i), s i j = t i j) : ⋂ (i : ι), ⋂ (j : κ i), s i j = ⋂ (i : ι), ⋂ (j : κ i), t i j

theorem Set.BijOn.iUnion_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} {f : β → γ} (g : γ → Set α) (hf : BijOn f s t) : ⋃ x ∈ s, g (f x) = ⋃ y ∈ t, g y

theorem Set.BijOn.iInter_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} {f : β → γ} (g : γ → Set α) (hf : BijOn f s t) : ⋂ x ∈ s, g (f x) = ⋂ y ∈ t, g y

theorem Set.BijOn.iUnion_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} (f : β → Set α) (g : γ → Set α) {h : β → γ} (h1 : BijOn h s t) (h2 : ∀ (x : β), g (h x) = f x) : ⋃ x ∈ s, f x = ⋃ y ∈ t, g y

theorem Set.BijOn.iInter_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} (f : β → Set α) (g : γ → Set α) {h : β → γ} (h1 : BijOn h s t) (h2 : ∀ (x : β), g (h x) = f x) : ⋂ x ∈ s, f x = ⋂ y ∈ t, g y

theorem Set.iUnion_const {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) : ⋃ (x : ι), s = s

theorem Set.iInter_const {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) : ⋂ (x : ι), s = s

theorem Set.iUnion_eq_const {α : Type u_1} {ι : Sort u_4} [Nonempty ι] {f : ι → Set α} {s : Set α} (hf : ∀ (i : ι), f i = s) : ⋃ (i : ι), f i = s

theorem Set.iInter_eq_const {α : Type u_1} {ι : Sort u_4} [Nonempty ι] {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 : ι) → κ i → Set α) : (⋃ (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 : ι) → κ i → Set α) : (⋂ (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 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 t : ι → Set β) : ⋂ (i : ι), s i ∩ t i = (⋂ (i : ι), s i) ∩ ⋂ (i : ι), t i

theorem Set.union_iUnion {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) (t : ι → Set β) : s ∪ ⋃ (i : ι), t i = ⋃ (i : ι), s ∪ t i

theorem Set.iUnion_union {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋃ (i : ι), t i) ∪ s = ⋃ (i : ι), t i ∪ s

theorem Set.inter_iInter {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) (t : ι → Set β) : s ∩ ⋂ (i : ι), t i = ⋂ (i : ι), s ∩ t i

theorem Set.iInter_inter {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋂ (i : ι), t i) ∩ s = ⋂ (i : ι), t i ∩ s

theorem Set.insert_iUnion {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (x : β) (t : ι → Set β) : insert x (⋃ (i : ι), t i) = ⋃ (i : ι), insert x (t i)

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.insert_iInter {β : Type u_2} {ι : Sort u_4} (x : β) (t : ι → Set β) : insert x (⋂ (i : ι), t i) = ⋂ (i : ι), insert x (t i)

theorem Set.iUnion_sdiff {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β) : (⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s

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

theorem Set.iUnion_diff {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β) : (⋃ (i : ι), t i) \ s = ⋃ (i : ι), t i \ s

Alias of Set.iUnion_sdiff.

theorem Set.sdiff_iUnion {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) (t : ι → Set β) : s \ ⋃ (i : ι), t i = ⋂ (i : ι), s \ t i

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

theorem Set.diff_iUnion {β : Type u_2} {ι : Sort u_4} [Nonempty ι] (s : Set β) (t : ι → Set β) : s \ ⋃ (i : ι), t i = ⋂ (i : ι), s \ t i

Alias of Set.sdiff_iUnion.

theorem Set.sdiff_iInter {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β) : s \ ⋂ (i : ι), t i = ⋃ (i : ι), s \ t i

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

theorem Set.diff_iInter {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β) : s \ ⋂ (i : ι), t i = ⋃ (i : ι), s \ t i

Alias of Set.sdiff_iInter.

theorem Set.iUnion_symmDiff_subset {α : Type u_1} {ι : Sort u_4} {s : Set α} [Nonempty ι] {f : ι → Set α} : symmDiff (⋃ (n : ι), f n) s ⊆ ⋃ (n : ι), symmDiff (f n) s

theorem Set.symmDiff_iUnion_subset {α : Type u_1} {ι : Sort u_4} {s : Set α} [Nonempty ι] {f : ι → Set α} : symmDiff s (⋃ (n : ι), f n) ⊆ ⋃ (n : ι), symmDiff s (f n)

theorem Set.iUnion_symmDiff_iUnion_subset {α : Type u_1} {ι : Sort u_4} {f g : ι → Set α} : symmDiff (⋃ (n : ι), f n) (⋃ (n : ι), g n) ⊆ ⋃ (n : ι), symmDiff (f n) (g n)

theorem Set.sUnion_symmDiff_subset {α : Type u_1} {s : Set α} {S : Set (Set α)} (hS : S.Nonempty) : symmDiff (⋃₀ S) s ⊆ ⋃₀ ((fun (x : Set α) => symmDiff x s) '' S)

theorem Set.symmDiff_sUnion_subset {α : Type u_1} {s : Set α} {S : Set (Set α)} (hS : S.Nonempty) : symmDiff s (⋃₀ S) ⊆ ⋃₀ ((fun (x : Set α) => symmDiff s x) '' S)

theorem Set.sUnion_symmDiff_sUnion_subset {α : Type u_1} {S T : Set (Set α)} (hS : S.Nonempty) (hT : T.Nonempty) : symmDiff (⋃₀ S) (⋃₀ T) ⊆ ⋃₀ image2 (fun (x1 x2 : Set α) => symmDiff x1 x2) S T

theorem Set.iUnion_inter_subset {ι : Sort u_9} {α : Type u_10} {s t : ι → Set α} : ⋃ (i : ι), s i ∩ t i ⊆ (⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i

theorem Set.iUnion_inter_of_monotone {ι : Type u_9} {α : Type u_10} [Preorder ι] [IsDirectedOrder ι] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) : ⋃ (i : ι), s i ∩ t i = (⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i

theorem Set.iUnion_inter_of_antitone {ι : Type u_9} {α : Type u_10} [Preorder ι] [IsCodirectedOrder ι] {s t : ι → Set α} (hs : Antitone s) (ht : Antitone t) : ⋃ (i : ι), s i ∩ t i = (⋃ (i : ι), s i) ∩ ⋃ (i : ι), t i

theorem Set.iInter_union_of_monotone {ι : Type u_9} {α : Type u_10} [Preorder ι] [IsCodirectedOrder ι] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) : ⋂ (i : ι), s i ∪ t i = (⋂ (i : ι), s i) ∪ ⋂ (i : ι), t i

theorem Set.iInter_union_of_antitone {ι : Type u_9} {α : Type u_10} [Preorder ι] [IsDirectedOrder ι] {s t : ι → Set α} (hs : Antitone s) (ht : Antitone t) : ⋂ (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_9} (s : Option ι → Set α) : ⋃ (o : Option ι), s o = s none ∪ ⋃ (i : ι), s (some i)

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

theorem Set.iUnion_dite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [DecidablePred p] (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

theorem Set.iUnion_ite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [DecidablePred p] (f 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) [DecidablePred p] (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

theorem Set.iInter_ite {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [DecidablePred p] (f g : ι → Set α) : (⋂ (i : ι), if p i then f i else g i) = (⋂ (i : ι), ⋂ (_ : p i), f i) ∩ ⋂ (i : ι), ⋂ (_ : ¬p i), g i

Unions and intersections indexed by Prop

theorem Set.iInter_false {α : Type u_1} {s : False → Set α} : iInter s = univ

theorem Set.iUnion_false {α : Type u_1} {s : False → Set α} : iUnion s = ∅

@[simp]

theorem Set.iInter_true {α : Type u_1} {s : True → Set α} : iInter s = s trivial

@[simp]

theorem Set.iUnion_true {α : Type u_1} {s : True → Set α} : iUnion s = s trivial

@[simp]

theorem Set.iInter_exists {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {f : Exists p → Set α} : ⋂ (x : Exists p), f x = ⋂ (i : ι), ⋂ (h : p i), f ⋯

@[simp]

theorem Set.iUnion_exists {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {f : Exists p → Set α} : ⋃ (x : Exists p), 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 : ι), univ = 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 = univ ↔ ∀ (i : ι), s i = 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 β} : (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty

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

theorem Set.iInter_or {α : Type u_1} {p q : Prop} (s : p ∨ q → Set α) : ⋂ (h : p ∨ q), s h = (⋂ (h : p), s ⋯) ∩ ⋂ (h : q), s ⋯

theorem Set.iUnion_or {α : Type u_1} {p q : Prop} (s : p ∨ q → Set α) : ⋃ (h : p ∨ q), s h = (⋃ (i : p), s ⋯) ∪ ⋃ (j : q), s ⋯

theorem Set.iUnion_and {α : Type u_1} {p q : Prop} (s : p ∧ q → Set α) : ⋃ (h : p ∧ q), s h = ⋃ (hp : p), ⋃ (hq : q), s ⋯

theorem Set.iInter_and {α : Type u_1} {p q : Prop} (s : p ∧ q → Set α) : ⋂ (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_9} (s : Sigma γ → Set β) : ⋃ (ia : Sigma γ), s ia = ⋃ (i : α), ⋃ (a : γ i), s ⟨i, a⟩

theorem Set.iUnion_sigma' {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : (i : α) → γ i → Set β) : ⋃ (i : α), ⋃ (a : γ i), s i a = ⋃ (ia : Sigma γ), s ia.fst ia.snd

theorem Set.iInter_sigma {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : Sigma γ → Set β) : ⋂ (ia : Sigma γ), s ia = ⋂ (i : α), ⋂ (a : γ i), s ⟨i, a⟩

theorem Set.iInter_sigma' {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : (i : α) → γ i → Set β) : ⋂ (i : α), ⋂ (a : γ i), s i a = ⋂ (ia : Sigma γ), s ia.fst ia.snd

theorem Set.iUnion₂_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_7} {κ' : ι' → Sort u_8} (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_5} {κ : ι → Sort u_7} {κ' : ι' → Sort u_8} (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 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 ⋯

@[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 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 ⋯

@[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 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 ⋯

@[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 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 ⋯

@[simp]

theorem Set.iUnion_iUnion_eq_or_left {α : Type u_1} {β : Type u_2} {b : β} {p : β → Prop} {s : (x : β) → x = b ∨ p x → Set α} : ⋃ (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 x → Set α} : ⋂ (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)

theorem Set.iUnion_psigma {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : PSigma γ → Set β) : ⋃ (ia : PSigma γ), s ia = ⋃ (i : α), ⋃ (a : γ i), s ⟨i, a⟩

theorem Set.iUnion_psigma' {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : (i : α) → γ i → Set β) : ⋃ (i : α), ⋃ (a : γ i), s i a = ⋃ (ia : PSigma γ), s ia.fst ia.snd

A reversed version of iUnion_psigma with a curried map.

theorem Set.iInter_psigma {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : PSigma γ → Set β) : ⋂ (ia : PSigma γ), s ia = ⋂ (i : α), ⋂ (a : γ i), s ⟨i, a⟩

theorem Set.iInter_psigma' {α : Type u_1} {β : Type u_2} {γ : α → Type u_9} (s : (i : α) → γ i → Set β) : ⋂ (i : α), ⋂ (a : γ i), s i a = ⋂ (ia : PSigma γ), s ia.fst ia.snd

A reversed version of iInter_psigma with a curried map.