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.iUnion_eq_sigma_of_disjoint: 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

instance Set.instInfSetSet {α : Type u_1} : InfSet (Set α)

instance Set.instSupSetSet {α : Type u_1} : SupSet (Set α)

def Set.sInter {α : Type u_1} (S : Set (Set α)) : Set α

Intersection of a set of sets.

def Set.«term⋂₀_» : Lean.ParserDescr

Notation for Set.sInter Intersection of a set of sets.

def Set.sUnion {α : Type u_1} (S : Set (Set α)) : Set α

Union of a set of sets.

def Set.«term⋃₀_» : Lean.ParserDescr

Notation for Set.sUnion. Union of a set of sets.

@[simp]

theorem Set.mem_sInter {α : Type u_1} {x : α} {S : Set (Set α)} : x ∈ ⋂₀ S ↔ ∀ (t : Set α), t ∈ S → x ∈ t

@[simp]

theorem Set.mem_sUnion {α : Type u_1} {x : α} {S : Set (Set α)} : x ∈ ⋃₀ S ↔ ∃ t, t ∈ S ∧ x ∈ t

def Set.iUnion {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) : Set β

Indexed union of a family of sets

def Set.iInter {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) : Set β

Indexed intersection of a family of sets

def Set.«term⋃_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

def Set.«term⋃_,_» : Lean.ParserDescr

Notation for Set.iUnion. Indexed union of a family of sets

def Set.«term⋂_,_» : Lean.ParserDescr

Notation for Set.iInter. Indexed intersection of a family of sets

def Set.«term⋂_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

@[simp]

theorem Set.sSup_eq_sUnion {α : Type u_1} (S : Set (Set α)) : sSup S = ⋃₀ S

@[simp]

theorem Set.sInf_eq_sInter {α : Type u_1} (S : Set (Set α)) : sInf S = ⋂₀ S

@[simp]

theorem Set.iSup_eq_iUnion {α : Type u_1} {ι : Sort u_4} (s : ι → Set α) : iSup s = Set.iUnion s

@[simp]

theorem Set.iInf_eq_iInter {α : Type u_1} {ι : Sort u_4} (s : ι → Set α) : iInf s = Set.iInter s

@[simp]

theorem Set.mem_iUnion {α : Type u_1} {ι : Sort u_4} {x : α} {s : ι → Set α} : x ∈ ⋃ (i : ι), s i ↔ ∃ i, x ∈ s i

@[simp]

theorem Set.mem_iInter {α : Type u_1} {ι : Sort u_4} {x : α} {s : ι → Set α} : x ∈ ⋂ (i : ι), s i ↔ ∀ (i : ι), x ∈ s i

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, 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

instance Set.Set.completeAtomicBooleanAlgebra {α : Type u_1} : CompleteAtomicBooleanAlgebra (Set α)

def Set.kernImage {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Set β

kernImage f s is the set of y such that f ⁻¹ y ⊆ s.

theorem Set.subset_kernImage_iff {α : Type u_1} {β : Type u_2} {s : Set β} {t : Set α} {f : α → β} : s ⊆ Set.kernImage f t ↔ f ⁻¹' s ⊆ t

theorem Set.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} : GaloisConnection (Set.image f) (Set.preimage f)

theorem Set.preimage_kernImage {α : Type u_1} {β : Type u_2} {f : α → β} : GaloisConnection (Set.preimage f) (Set.kernImage f)

theorem Set.kernImage_mono {α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (Set.kernImage f)

theorem Set.kernImage_eq_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : Set.kernImage f s = (f '' sᶜ)ᶜ

theorem Set.kernImage_compl {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : Set.kernImage f sᶜ = (f '' s)ᶜ

theorem Set.kernImage_empty {α : Type u_1} {β : Type u_2} {f : α → β} : Set.kernImage f ∅ = (Set.range f)ᶜ

theorem Set.kernImage_preimage_eq_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : Set.kernImage f (f ⁻¹' s) = s ↔ (Set.range f)ᶜ ⊆ s

theorem Set.compl_range_subset_kernImage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} : (Set.range f)ᶜ ⊆ Set.kernImage f s

theorem Set.kernImage_union_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Set.kernImage f (s ∪ f ⁻¹' t) = Set.kernImage f s ∪ t

theorem Set.kernImage_preimage_union {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Set.kernImage f (f ⁻¹' t ∪ s) = t ∪ Set.kernImage f s

Union and intersection over an indexed family of sets

instance Set.instOrderTopSetInstLESet {α : Type u_1} : OrderTop (Set α)

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

theorem Set.iInter_congr_Prop {α : Type u_1} {p : Prop} {q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) : Set.iInter f₁ = Set.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 α) : ⋃ (x : 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 α) : ⋂ (x : p), s = if p then s else Set.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 Set.univ

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

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

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

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

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 : ι) → κ 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.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_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 : ι) → κ 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 : ι → 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) : Set.iUnion s ⊆ Set.iUnion t

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

theorem Set.iInter₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {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_10} {s : (i : ι) → κ i → Set α} {t : (i' : ι') → κ' i' → Set α} (h : ∀ (i : ι) (j : κ i), ∃ i' j', 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 : ι) → κ i → Set α} {t : (i' : ι') → κ' i' → Set α} (h : ∀ (i' : ι') (j' : κ' i'), ∃ i j, 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 : 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 : ι → 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 : ι) → κ i → Set α} {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 : (i : ι) → κ i → Set α} {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_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 : ι → 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} [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.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} [Nonempty ι] (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.directed_on_iUnion {α : Type u_1} {ι : Sort u_4} {r : α → α → Prop} {f : ι → Set α} (hd : Directed (fun x x_1 => x ⊆ x_1) f) (h : ∀ (x : ι), DirectedOn r (f x)) : DirectedOn r (⋃ (x : ι), f x)

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} [Preorder ι] [IsDirected ι fun x x_1 => x ≤ x_1] {s : ι → Set α} {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_11} {α : Type u_12} [Preorder ι] [IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)] {s : ι → Set α} {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_11} {α : Type u_12} [Preorder ι] [IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)] {s : ι → Set α} {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_11} {α : Type u_12} [Preorder ι] [IsDirected ι fun x x_1 => x ≤ x_1] {s : ι → Set α} {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_11} (s : Option ι → Set α) : ⋃ (o : Option ι), s o = s none ∪ ⋃ (i : ι), s (some i)

theorem Set.iInter_option {α : Type u_1} {ι : Type u_11} (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 : ι → Set α) (g : ι → Set α) : (⋃ (i : ι), if p i then f i else g i) = (⋃ (i : ι) (x : 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 : ι → Set α) (g : ι → Set α) : (⋂ (i : ι), if p i then f i else g i) = (⋂ (i : ι) (x : 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.Nonempty (Set.pi Set.univ v)) (i : ι) : (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k = v i

Unions and intersections indexed by Prop

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

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

@[simp]

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

@[simp]

theorem Set.iUnion_true {α : Type u_1} {s : True → Set α} : 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 (_ : Exists p)

@[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 (_ : Exists p)

@[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 α} : Set.Nonempty (⋃ (i : ι), s i) ↔ ∃ i, Set.Nonempty (s i)

theorem Set.nonempty_biUnion {α : Type u_1} {β : Type u_2} {t : Set α} {s : α → Set β} : Set.Nonempty (⋃ (i : α) (_ : i ∈ t), s i) ↔ ∃ i, i ∈ t ∧ Set.Nonempty (s i)

theorem Set.iUnion_nonempty_index {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set.Nonempty s → Set β) : ⋃ (h : Set.Nonempty s), t h = ⋃ (x : α) (h : x ∈ s), t (_ : ∃ x, x ∈ s)

@[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 (_ : b = 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 (_ : b = 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 (_ : b = 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 (_ : b = b)

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

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

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

theorem Set.iInter_and {α : Type u_1} {p : Prop} {q : Prop} (s : p ∧ q → Set α) : ⋂ (h : p ∧ q), s h = ⋂ (hp : p) (hq : q), s (_ : p ∧ q)

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₂_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 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 (_ : p x ∧ q 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 (_ : p y ∧ q 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 (_ : p x ∧ q 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 (_ : p y ∧ q 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 (_ : b = b ∨ p b) ∪ ⋃ (x : β) (h : p x), s x (_ : x = b ∨ p 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 (_ : b = b ∨ p b) ∩ ⋂ (x : β) (h : p x), s x (_ : x = b ∨ p 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 ∈ ⋃ (x : α) (_ : 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 : α), x ∈ s → y ∈ t x) : y ∈ ⋂ (x : α) (_ : 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 : α) (_ : 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 : α) (_ : x ∈ s), 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') : ⋃ (x : α) (_ : x ∈ s), t x ⊆ ⋃ (x : α) (_ : x ∈ s'), t x

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

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

theorem Set.biInter_mono {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : α → Set β} {t' : α → Set β} (hs : s ⊆ s') (h : ∀ (x : α), x ∈ s → t x ⊆ t' x) : ⋂ (x : α) (_ : x ∈ s'), t x ⊆ ⋂ (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 (_ : ↑x ∈ s)

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 (_ : ↑x ∈ s)

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 { val := x, property := 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 { val := x, property := hx }

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

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

@[simp]

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

@[simp]

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

theorem Set.biInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β) : ⋂ (x : α) (_ : x ∈ {a}), s x = s a

theorem Set.biInter_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : α → Set β) : ⋂ (x : α) (_ : x ∈ s ∪ t), u x = (⋂ (x : α) (_ : x ∈ s), u x) ∩ ⋂ (x : α) (_ : x ∈ t), u x

theorem Set.biInter_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β) : ⋂ (x : α) (_ : x ∈ insert a s), t x = t a ∩ ⋂ (x : α) (_ : x ∈ s), t x

theorem Set.biInter_pair {α : Type u_1} {β : Type u_2} (a : α) (b : α) (s : α → Set β) : ⋂ (x : α) (_ : x ∈ {a, b}), s x = s a ∩ s b

theorem Set.biInter_inter {ι : Type u_11} {α : Type u_12} {s : Set ι} (hs : Set.Nonempty s) (f : ι → Set α) (t : Set α) : ⋂ (i : ι) (_ : i ∈ s), f i ∩ t = (⋂ (i : ι) (_ : i ∈ s), f i) ∩ t

theorem Set.inter_biInter {ι : Type u_11} {α : Type u_12} {s : Set ι} (hs : Set.Nonempty s) (f : ι → Set α) (t : Set α) : ⋂ (i : ι) (_ : i ∈ s), t ∩ f i = t ∩ ⋂ (i : ι) (_ : i ∈ s), f i

theorem Set.biUnion_empty {α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ (x : α) (_ : x ∈ ∅), s x = ∅

theorem Set.biUnion_univ {α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ (x : α) (_ : x ∈ Set.univ), s x = ⋃ (x : α), s x

theorem Set.biUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β) : ⋃ (x : α) (_ : x ∈ {a}), s x = s a

@[simp]

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

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

@[simp]

theorem Set.iUnion_coe_set {α : Type u_11} {β : Type u_12} (s : Set α) (f : ↑s → Set β) : ⋃ (i : ↑s), f i = ⋃ (i : α) (h : i ∈ s), f { val := i, property := h }

@[simp]

theorem Set.iInter_coe_set {α : Type u_11} {β : Type u_12} (s : Set α) (f : ↑s → Set β) : ⋂ (i : ↑s), f i = ⋂ (i : α) (h : i ∈ s), f { val := i, property := h }

theorem Set.biUnion_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β) : ⋃ (x : α) (_ : x ∈ insert a s), t x = t a ∪ ⋃ (x : α) (_ : x ∈ s), t x

theorem Set.biUnion_pair {α : Type u_1} {β : Type u_2} (a : α) (b : α) (s : α → Set β) : ⋃ (x : α) (_ : 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 : ι) → κ 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_7} (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_7} (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_7} (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.not_mem_of_not_mem_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' : Set α), t' ∈ S → t' ⊆ t) : ⋃₀ S ⊆ t

@[simp]

theorem Set.sUnion_subset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} : ⋃₀ s ⊆ t ↔ ∀ (t' : Set α), t' ∈ s → t' ⊆ t

theorem Set.subset_sInter {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : ∀ (t' : Set α), t' ∈ S → t ⊆ t') : t ⊆ ⋂₀ S

@[simp]

theorem Set.subset_sInter_iff {α : Type u_1} {S : Set (Set α)} {t : Set α} : t ⊆ ⋂₀ S ↔ ∀ (t' : Set α), t' ∈ S → t ⊆ t'

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

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

@[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 = ∅ ↔ ∀ (s : Set α), s ∈ S → s = ∅

@[simp]

theorem Set.sInter_eq_univ {α : Type u_1} {S : Set (Set α)} : ⋂₀ S = Set.univ ↔ ∀ (s : Set α), s ∈ S → s = Set.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 => ⋃₀ x) fun x => 𝒫 x

⋃₀ and 𝒫 form a Galois connection.

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

⋃₀ and 𝒫 form a Galois insertion.

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 α)} : Set.Nonempty (⋃₀ S) ↔ ∃ s, s ∈ S ∧ Set.Nonempty s

theorem Set.Nonempty.of_sUnion {α : Type u_1} {s : Set (Set α)} (h : Set.Nonempty (⋃₀ s)) : Set.Nonempty s

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

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

theorem Set.sInter_union {α : Type u_1} (S : Set (Set α)) (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_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) = ⋃ (x : α) (_ : x ∈ s), f x

@[simp]

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

@[simp]

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

@[simp]

theorem Set.sInter_range {β : Type u_2} {ι : Sort u_4} (f : ι → Set β) : ⋂₀ Set.range f = ⋂ (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 : ι) → κ i → Set α} : ⋃ (i : ι) (j : κ i), s i j = Set.univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j

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

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_7} {s : (i : ι) → κ i → Set α} : ⋂ (i : ι) (j : κ i), s i j = ∅ ↔ ∀ (a : α), ∃ i j, ¬a ∈ s i j

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

@[simp]

theorem Set.nonempty_iInter {α : Type u_1} {ι : Sort u_4} {f : ι → Set α} : Set.Nonempty (⋂ (i : ι), f i) ↔ ∃ x, ∀ (i : ι), x ∈ f i

theorem Set.nonempty_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} : Set.Nonempty (⋂ (i : ι) (j : κ i), s i j) ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j

@[simp]

theorem Set.nonempty_sInter {α : Type u_1} {c : Set (Set α)} : Set.Nonempty (⋂₀ c) ↔ ∃ a, ∀ (b : Set α), 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 : 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 : Sigma γ → β) : Set.range f = ⋃ (a : α), Set.range fun b => f { fst := a, snd := b }

theorem Set.iUnion_eq_range_sigma {α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ (i : α), s i = Set.range fun a => ↑a.snd

theorem Set.iUnion_eq_range_psigma {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) : ⋃ (i : ι), s i = Set.range fun a => ↑a.snd

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

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

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

Alias of Set.sUnion_subset_sUnion.

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} = Set.range f

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 = ⋃ (i : Set α) (_ : i ∈ s), i

theorem Set.sInter_eq_biInter {α : Type u_1} {s : Set (Set α)} : ⋂₀ s = ⋂ (i : Set α) (_ : 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 = 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 = ⋂ (p : Set α × Set α) (_ : p ∈ S ×ˢ T), p.fst ∪ p.snd

theorem Set.sUnion_inter_sUnion {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} : ⋃₀ s ∩ ⋃₀ t = ⋃ (p : Set α × Set α) (_ : p ∈ s ×ˢ t), p.fst ∩ p.snd

theorem Set.biUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι → Set α) (t : α → Set β) : ⋃ (x : α) (_ : x ∈ ⋃ (i : ι), s i), t x = ⋃ (i : ι) (x : α) (_ : x ∈ s i), t x

theorem Set.biInter_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι → Set α) (t : α → Set β) : ⋂ (x : α) (_ : x ∈ ⋃ (i : ι), s i), t x = ⋂ (i : ι) (x : α) (_ : 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_11} {β : Type u_12} (C : Set (Set α)) {f : (s : ↑C) → β → ↑↑s} (hf : ∀ (s : ↑C), Function.Surjective (f s)) : (⋃ (y : β), Set.range fun s => ↑(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 : ι) → κ 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_7} (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι) (j : κ i), s i j) ∪ t = ⋂ (i : ι) (j : κ i), s i j ∪ t

mapsTo

theorem Set.mapsTo_sUnion {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : α → β} (H : ∀ (s : Set α), s ∈ S → Set.MapsTo f s t) : Set.MapsTo f (⋃₀ S) t

theorem Set.mapsTo_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : Set β} {f : α → β} (H : ∀ (i : ι), Set.MapsTo f (s i) t) : Set.MapsTo f (⋃ (i : ι), s i) t

theorem Set.mapsTo_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t) : Set.MapsTo f (⋃ (i : ι) (j : κ i), 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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {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.mapsTo_sInter {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β} (H : ∀ (t : Set β), t ∈ T → Set.MapsTo f s t) : Set.MapsTo f s (⋂₀ T)

theorem Set.mapsTo_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), Set.MapsTo f s (t i)) : Set.MapsTo f s (⋂ (i : ι), t i)

theorem Set.mapsTo_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)) : Set.MapsTo f s (⋂ (i : ι) (j : κ i), 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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {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 : ι) → κ i → Set α) (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 ⊆ ⋂ (s : Set α) (_ : s ∈ S), 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.iUnion U = Set.univ) : Function.Injective f ↔ ∀ (i : ι), Function.Injective (Set.restrictPreimage (U i) f)

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

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

InjOn

theorem Set.InjOn.image_iInter_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Nonempty ι] {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 i → Set α} (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 : Function.Bijective f) (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 : Function.Bijective f) (s : (i : ι) → κ i → Set α) : 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 x x_1 => x ⊆ x_1) 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 : ∀ (t : Set β), t ∈ T → Set.SurjOn f s t) : 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 : ι) → κ i → Set β} {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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {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} [Nonempty ι] {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} [Nonempty ι] {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 : Nonempty ι] {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 x x_1 => x ⊆ x_1) 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} [Nonempty ι] {s : ι → Set α} (hs : Directed (fun x x_1 => x ⊆ x_1) 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 : ι) → κ i → Set α) : 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), {{ val := x, property := h }}

theorem Set.range_eq_iUnion {α : Type u_1} {ι : Sort u_11} (f : ι → α) : Set.range f = ⋃ (i : ι), {f i}

theorem Set.image_eq_iUnion {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : f '' s = ⋃ (i : α) (_ : i ∈ s), {f i}

theorem Set.biUnion_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β} : ⋃ (x : α) (_ : x ∈ Set.range f), 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 : α) (_ : x ∈ Set.range f), 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 β} : ⋃ (x : α) (_ : x ∈ f '' s), g x = ⋃ (y : γ) (_ : y ∈ s), g (f y)

theorem Set.biInter_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β} : ⋂ (x : α) (_ : x ∈ f '' s), g x = ⋂ (y : γ) (_ : y ∈ s), g (f y)

theorem Set.monotone_preimage {α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (Set.preimage 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 : ι) → κ i → Set β} : f ⁻¹' ⋃ (i : ι) (j : κ i), s i j = ⋃ (i : ι) (j : κ i), f ⁻¹' s i j

@[simp]

theorem Set.preimage_sUnion {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀ s = ⋃ (t : Set β) (_ : t ∈ s), 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 : ι) → κ i → Set β} : 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 = ⋂ (t : Set β) (_ : t ∈ s), f ⁻¹' t

@[simp]

theorem Set.biUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : ⋃ (y : β) (_ : y ∈ s), f ⁻¹' {y} = f ⁻¹' s

theorem Set.biUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) : ⋃ (y : β) (_ : y ∈ Set.range f), 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 : ι) → κ i → Set β} : 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 => 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 : ι) → κ i → Set α} {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 => 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.fst ×ˢ t x.snd = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i

theorem Set.iUnion_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) : ⋃ (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 ⊆ ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd

theorem Set.sInter_prod_sInter {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {T : Set (Set β)} (hS : Set.Nonempty S) (hT : Set.Nonempty T) : ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd

theorem Set.sInter_prod {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : Set.Nonempty S) (t : Set β) : ⋂₀ S ×ˢ t = ⋂ (s : Set α) (_ : s ∈ S), s ×ˢ t

theorem Set.prod_sInter {α : Type u_1} {β : Type u_2} {T : Set (Set β)} (hT : Set.Nonempty T) (s : Set α) : s ×ˢ ⋂₀ T = ⋂ (t : Set β) (_ : t ∈ T), s ×ˢ t

theorem Set.iUnion_image_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β} : ⋃ (a : α) (_ : a ∈ s), 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 β} : ⋃ (b : β) (_ : b ∈ t), (fun a => f a 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 : ι) → κ i → Set α) (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 : ι) → κ i → Set β) : 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 : ι) → κ i → Set α) (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 : ι) → κ i → Set β) : Set.image2 f s (⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), Set.image2 f s (t i j)

theorem Set.image2_eq_iUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) : Set.image2 f s t = ⋃ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), {f i j}

The Set.image2 version of Set.image_eq_iUnion

theorem Set.prod_eq_biUnion_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = ⋃ (a : α) (_ : a ∈ s), (fun b => (a, b)) '' t

theorem Set.prod_eq_biUnion_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = ⋃ (b : β) (_ : b ∈ t), (fun a => (a, b)) '' s

def Set.seq {α : Type u_1} {β : Type u_2} (s : Set (α → β)) (t : Set α) : Set β

Given a set s of functions α → β and t : Set α, seq s t is the union of f '' t over all f ∈ s.

theorem Set.seq_def {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} : Set.seq s t = ⋃ (f : α → β) (_ : f ∈ s), f '' t

@[simp]

theorem Set.mem_seq_iff {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} {b : β} : b ∈ Set.seq s t ↔ ∃ f, f ∈ s ∧ ∃ a, a ∈ t ∧ f a = b

theorem Set.seq_subset {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} {u : Set β} : Set.seq s t ⊆ u ↔ ∀ (f : α → β), f ∈ s → ∀ (a : α), a ∈ t → 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₁) : Set.seq s₀ t₀ ⊆ Set.seq s₁ t₁

theorem Set.singleton_seq {α : Type u_1} {β : Type u_2} {f : α → β} {t : Set α} : Set.seq {f} t = f '' t

theorem Set.seq_singleton {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {a : α} : Set.seq s {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 α} : Set.seq s (Set.seq t u) = Set.seq (Set.seq ((fun x x_1 => x ∘ x_1) '' s) t) u

theorem Set.image_seq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {s : Set (α → β)} {t : Set α} : f '' Set.seq s t = Set.seq ((fun x x_1 => x ∘ x_1) f '' s) t

theorem Set.prod_eq_seq {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = Set.seq (Prod.mk '' s) t

theorem Set.prod_image_seq_comm {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Set.seq (Prod.mk '' s) t = Set.seq ((fun b a => (a, b)) '' t) 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 = Set.seq (f '' s) t

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

theorem Set.univ_pi_eq_iInter {α : Type u_1} {π : α → Type u_11} (t : (i : α) → Set (π i)) : Set.pi Set.univ t = ⋂ (i : α), Function.eval 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)) : Set.pi i s \ Set.pi i t ⊆ ⋃ (a : α) (_ : a ∈ i), Function.eval a ⁻¹' (s a \ t a)

theorem Set.iUnion_univ_pi {α : Type u_1} {ι : Sort u_4} {π : α → Type u_11} (t : (i : α) → ι → Set (π i)) : (⋃ (x : α → ι), Set.pi Set.univ fun i => t i (x i)) = Set.pi Set.univ fun i => ⋃ (j : ι), t i j

theorem Function.Surjective.iUnion_comp {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι → ι₂} (hf : Function.Surjective f) (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 : Function.Surjective f) (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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} : 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 ↔ ∀ (s : Set α), s ∈ S → Disjoint s t

@[simp]

theorem Set.disjoint_sUnion_right {α : Type u_1} {s : Set α} {S : Set (Set α)} : Disjoint s (⋃₀ S) ↔ ∀ (t : Set α), t ∈ S → Disjoint s t

Intervals

theorem Set.nonempty_iInter_Iic_iff {α : Type u_1} {ι : Sort u_4} [Preorder α] {f : ι → α} : Set.Nonempty (⋂ (i : ι), Set.Iic (f i)) ↔ BddBelow (Set.range f)

theorem Set.nonempty_iInter_Ici_iff {α : Type u_1} {ι : Sort u_4} [Preorder α] {f : ι → α} : Set.Nonempty (⋂ (i : ι), Set.Ici (f i)) ↔ BddAbove (Set.range f)

theorem Set.Ici_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) : Set.Ici (⨆ (i : ι), f i) = ⋂ (i : ι), Set.Ici (f i)

theorem Set.Iic_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) : Set.Iic (⨅ (i : ι), f i) = ⋂ (i : ι), Set.Iic (f i)

theorem Set.Ici_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} [CompleteLattice α] (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} [CompleteLattice α] (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} [CompleteLattice α] (s : Set α) : Set.Ici (sSup s) = ⋂ (a : α) (_ : a ∈ s), Set.Ici a

theorem Set.Iic_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) : Set.Iic (sInf s) = ⋂ (a : α) (_ : a ∈ s), Set.Iic a

theorem Set.biUnion_diff_biUnion_subset {α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ : Set α) (s₂ : Set α) : (⋃ (x : α) (_ : x ∈ s₁), t x) \ ⋃ (x : α) (_ : x ∈ s₂), t x ⊆ ⋃ (x : α) (_ : x ∈ s₁ \ 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.

theorem Set.sigmaToiUnion_surjective {α : Type u_1} {β : Type u_2} (t : α → Set β) : Function.Surjective (Set.sigmaToiUnion t)

theorem Set.sigmaToiUnion_injective {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)) : Function.Injective (Set.sigmaToiUnion t)

theorem Set.sigmaToiUnion_bijective {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)) : Function.Bijective (Set.sigmaToiUnion t)

noncomputable def Set.unionEqSigmaOfDisjoint {α : Type u_1} {β : Type u_2} {t : α → Set β} (h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)) : ↑(⋃ (i : α), t i) ≃ (i : α) × ↑(t i)

Equivalence between a disjoint union and a dependent sum.

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 : Monotone f) (k : ℕ) : ⋃ (n : ℕ), f (n + k) = ⋃ (n : ℕ), f n

theorem Antitone.iInter_nat_add {α : Type u_1} {f : ℕ → Set α} (hf : Antitone f) (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} [CompleteLattice β] (s : ι → Set α) (f : α → β) : ⨆ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a = ⨆ (i : ι) (a : α) (_ : a ∈ s i), f a

theorem iInf_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice β] (s : ι → Set α) (f : α → β) : ⨅ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a = ⨅ (i : ι) (a : α) (_ : a ∈ s i), f a

theorem sSup_sUnion {β : Type u_2} [CompleteLattice β] (s : Set (Set β)) : sSup (⋃₀ s) = ⨆ (t : Set β) (_ : t ∈ s), sSup t

theorem sInf_sUnion {β : Type u_2} [CompleteLattice β] (s : Set (Set β)) : sInf (⋃₀ s) = ⨅ (t : Set β) (_ : t ∈ s), sInf t

theorem iSup_sUnion {α : Type u_1} {β : Type u_2} [CompleteLattice β] (S : Set (Set α)) (f : α → β) : ⨆ (x : α) (_ : x ∈ ⋃₀ S), f x = ⨆ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), f x

theorem iInf_sUnion {α : Type u_1} {β : Type u_2} [CompleteLattice β] (S : Set (Set α)) (f : α → β) : ⨅ (x : α) (_ : x ∈ ⋃₀ S), f x = ⨅ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), f x

theorem forall_sUnion {α : Type u_1} {S : Set (Set α)} {p : α → Prop} : ((x : α) → x ∈ ⋃₀ S → p x) ↔ (s : Set α) → s ∈ S → (x : α) → x ∈ s → p x

theorem exists_sUnion {α : Type u_1} {S : Set (Set α)} {p : α → Prop} : (∃ x, x ∈ ⋃₀ S ∧ p x) ↔ ∃ s, s ∈ S ∧ ∃ x, x ∈ s ∧ p x