Documentation

instance Set.instInfSetSet {α : Type u_1} :

InfSet (Set α)

Equations

Set.instInfSetSet = { sInf := fun (s : Set (Set α)) => {a : α | ∀ t ∈ s, a ∈ t} }

instance Set.instSupSetSet {α : Type u_1} :

SupSet (Set α)

Equations

Set.instSupSetSet = { sSup := fun (s : Set (Set α)) => {a : α | ∃ t ∈ s, a ∈ t} }

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

Set α

Intersection of a set of sets.

Equations

⋂₀ S = sInf S

Instances For

def Set.«term⋂₀_» :

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

Equations

Set.«term⋂₀_» = Lean.ParserDescr.node `Set.term⋂₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

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

Set α

Union of a set of sets.

Equations

⋃₀ S = sSup S

Instances For

def Set.«term⋃₀_» :

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

Equations

Set.«term⋃₀_» = Lean.ParserDescr.node `Set.term⋃₀_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

Instances For

@[simp]

theorem Set.mem_sInter {α : Type u_1} {x : α} {S : Set (Set α)} :

x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t

@[simp]

theorem Set.mem_sUnion {α : Type u_1} {x : α} {S : Set (Set α)} :

x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t

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

Set β

Indexed union of a family of sets

Equations

Set.iUnion s = iSup s

Instances For

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

Set β

Indexed intersection of a family of sets

Equations

Set.iInter s = iInf s

Instances For

def Set.«term⋃_,_».delab :

Pretty printer defined by notation3 command.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Set.«term⋃_,_» :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def Set.«term⋂_,_».delab :

Pretty printer defined by notation3 command.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Set.«term⋂_,_» :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def Set.iUnion_delab :

Delaborator for indexed unions.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Set.sInter_delab :

Delaborator for indexed intersections.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[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 : κ 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

instance Set.completeAtomicBooleanAlgebra {α : Type u_1} :

CompleteAtomicBooleanAlgebra (Set α)

Equations

One or more equations did not get rendered due to their size.

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 α)

Equations

Set.instOrderTopSetInstLESet = OrderTop.mk (_ : ∀ (a : Set α), a ⊆ Set.univ)

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₁ (_ : p) = 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₁ (_ : p) = 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 α) :

⋃ (_ : 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 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 ∈ t, s i = ⊤) (x : β) :

∃ 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 ∈ 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' : κ' i'), s i j ⊆ t i' j') :

⋃ (i : ι), ⋃ (j : κ i), s i j ⊆ ⋃ (i' : ι'), ⋃ (j' : κ' i'), t i' j'

theorem Set.iInter_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {s : ι → Set α} {t : ι' → Set α} (h : ∀ (j : ι'), ∃ (i : ι), s i ⊆ t j) :

⋂ (i : ι), s i ⊆ ⋂ (j : ι'), t j

theorem Set.iInter₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_7} {κ' : ι' → Sort u_10} {s : (i : ι) → κ 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_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 : Set α) => 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 : ι), ⋃ (_ : 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 : ι), ⋂ (_ : 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 : (i : ι) → α i) => x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) => x k) ⁻¹' v k = v i

Unions and intersections indexed by `Prop` #

theorem Set.iInter_false {α : Type u_1} {s : 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 ∈ t, s 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 ∈ s, t x

A specialization of mem_iUnion₂.

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

y ∈ ⋂ x ∈ s, t x

A specialization of mem_iInter₂.

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

u x ⊆ ⋃ x ∈ s, u x

A specialization of subset_iUnion₂.

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

⋂ x ∈ s, t x ⊆ t x

A specialization of iInter₂_subset.

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

⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x

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

⋂ x ∈ s, t x ⊆ ⋂ x ∈ s', t x

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

⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x

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

⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x

theorem Set.biUnion_eq_iUnion {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β) :

⋃ (x : α), ⋃ (h : x ∈ s), t x h = ⋃ (x : ↑s), t ↑x (_ : ↑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 ∈ ∅, u x = Set.univ

theorem Set.biInter_univ {α : Type u_1} {β : Type u_2} (u : α → Set β) :

⋂ x ∈ Set.univ, u x = ⋂ (x : α), u x

@[simp]

theorem Set.biUnion_self {α : Type u_1} (s : Set α) :

⋃ x ∈ s, s = s

@[simp]

theorem Set.iUnion_nonempty_self {α : Type u_1} (s : Set α) :

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

theorem Set.biInter_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β) :

⋂ x ∈ {a}, s x = s a

theorem Set.biInter_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : α → Set β) :

⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x

theorem Set.biInter_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β) :

⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x

theorem Set.biInter_pair {α : Type u_1} {β : Type u_2} (a : α) (b : α) (s : α → Set β) :

⋂ x ∈ {a, b}, s x = s a ∩ s b

theorem Set.biInter_inter {ι : Type u_11} {α : Type u_12} {s : Set ι} (hs : Set.Nonempty s) (f : ι → Set α) (t : Set α) :

⋂ i ∈ s, f i ∩ t = (⋂ 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 ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i

theorem Set.biUnion_empty {α : Type u_1} {β : Type u_2} (s : α → Set β) :

⋃ x ∈ ∅, s x = ∅

theorem Set.biUnion_univ {α : Type u_1} {β : Type u_2} (s : α → Set β) :

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

theorem Set.biUnion_singleton {α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β) :

⋃ x ∈ {a}, s x = s a

@[simp]

theorem Set.biUnion_of_singleton {α : Type u_1} (s : Set α) :

⋃ x ∈ s, {x} = s

theorem Set.biUnion_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : α → Set β) :

⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x

@[simp]

theorem Set.iUnion_coe_set {α : Type u_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 ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x

theorem Set.biUnion_pair {α : Type u_1} {β : Type u_2} (a : α) (b : α) (s : α → Set β) :

⋃ x ∈ {a, b}, s x = s a ∪ s b

theorem Set.inter_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_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' ∈ S, t' ⊆ t) :

⋃₀ S ⊆ t

@[simp]

theorem Set.sUnion_subset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} :

⋃₀ s ⊆ t ↔ ∀ t' ∈ s, t' ⊆ t

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

⋃₀ s ⊆ ⋃₀ (f '' s)

sUnion is monotone under taking a subset of each set.

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

⋃₀ (f '' s) ⊆ ⋃₀ s

sUnion is monotone under taking a superset of each set.

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

t ⊆ ⋂₀ S

@[simp]

theorem Set.subset_sInter_iff {α : Type u_1} {S : Set (Set α)} {t : Set α} :

t ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t'

theorem Set.sUnion_subset_sUnion {α : Type u_1} {S : 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 ∈ S, s = ∅

@[simp]

theorem Set.sInter_eq_univ {α : Type u_1} {S : Set (Set α)} :

⋂₀ S = Set.univ ↔ ∀ 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 : Set (Set α)) => ⋃₀ x) fun (x : Set α) => 𝒫 x

⋃₀ and 𝒫 form a Galois connection.

def Set.sUnion_powerset_gi {α : Type u_1} :

GaloisInsertion (fun (x : Set (Set α)) => ⋃₀ x) fun (x : Set α) => 𝒫 x

⋃₀ and 𝒫 form a Galois insertion.

Equations

Set.sUnion_powerset_gi = gi_sSup_Iic

Instances For

theorem Set.sUnion_mem_empty_univ {α : Type u_1} {S : Set (Set α)} (h : S ⊆ {∅, Set.univ}) :

⋃₀ S ∈ {∅, Set.univ}

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

@[simp]

theorem Set.nonempty_sUnion {α : Type u_1} {S : Set (Set α)} :

Set.Nonempty (⋃₀ 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 ∈ s, f x

@[simp]

theorem Set.sInter_image {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α) :

⋂₀ (f '' s) = ⋂ 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 : κ i), a ∈ s i j

theorem Set.sUnion_eq_univ_iff {α : Type u_1} {c : Set (Set α)} :

⋃₀ c = Set.univ ↔ ∀ (a : α), ∃ 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 : κ i), a ∉ s i j

theorem Set.sInter_eq_empty_iff {α : Type u_1} {c : Set (Set α)} :

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

@[simp]

theorem Set.nonempty_iInter {α : Type u_1} {ι : Sort u_4} {f : ι → Set α} :

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 ∈ 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 : γ a) => 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 : (i : α) × ↑(s i)) => ↑a.snd

theorem Set.iUnion_eq_range_psigma {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) :

⋃ (i : ι), s i = Set.range fun (a : (i : ι) ×' ↑(s i)) => ↑a.snd

theorem Set.iUnion_image_preimage_sigma_mk_eq_self {ι : Type u_11} {σ : ι → Type u_12} (s : Set (Sigma σ)) :

⋃ (i : ι), 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 ∈ s, i

theorem Set.sInter_eq_biInter {α : Type u_1} {s : Set (Set α)} :

⋂₀ s = ⋂ i ∈ s, i

theorem Set.sUnion_eq_iUnion {α : Type u_1} {s : Set (Set α)} :

⋃₀ s = ⋃ (i : ↑s), ↑i

theorem Set.sInter_eq_iInter {α : Type u_1} {s : Set (Set α)} :

⋂₀ s = ⋂ (i : ↑s), ↑i

@[simp]

theorem Set.iUnion_of_empty {α : Type u_1} {ι : Sort u_4} [IsEmpty ι] (s : ι → Set α) :

⋃ (i : ι), s i = ∅

@[simp]

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

⋂ (i : ι), s i = 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 ∈ S ×ˢ T, p.1 ∪ p.2

theorem Set.sUnion_inter_sUnion {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} :

⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, p.1 ∩ p.2

theorem Set.biUnion_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι → Set α) (t : α → Set β) :

⋃ x ∈ ⋃ (i : ι), s i, t x = ⋃ (i : ι), ⋃ x ∈ s i, t x

theorem Set.biInter_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (s : ι → Set α) (t : α → Set β) :

⋂ x ∈ ⋃ (i : ι), s i, t x = ⋂ (i : ι), ⋂ x ∈ s i, t x

theorem Set.sUnion_iUnion {α : Type u_1} {ι : Sort u_4} (s : ι → Set (Set α)) :

⋃₀ ⋃ (i : ι), s i = ⋃ (i : ι), ⋃₀ s i

theorem Set.sInter_iUnion {α : Type u_1} {ι : Sort u_4} (s : ι → Set (Set α)) :

⋂₀ ⋃ (i : ι), s i = ⋂ (i : ι), ⋂₀ s i

theorem Set.iUnion_range_eq_sUnion {α : Type u_11} {β : Type u_12} (C : Set (Set α)) {f : (s : ↑C) → β → ↑↑s} (hf : ∀ (s : ↑C), Function.Surjective (f s)) :

(⋃ (y : β), Set.range fun (s : ↑C) => ↑(f s y)) = ⋃₀ C

theorem Set.iUnion_range_eq_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (C : ι → Set α) {f : (x : ι) → β → ↑(C x)} (hf : ∀ (x : ι), Function.Surjective (f x)) :

(⋃ (y : β), Set.range fun (x : ι) => ↑(f x y)) = ⋃ (x : ι), C x

theorem Set.union_distrib_iInter_left {α : Type u_1} {ι : Sort u_4} (s : ι → Set α) (t : Set α) :

t ∪ ⋂ (i : ι), s i = ⋂ (i : ι), t ∪ s i

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

Lemmas about `Set.MapsTo` #

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

@[simp]

theorem Set.mapsTo_sUnion {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : α → β} :

Set.MapsTo f (⋃₀ S) t ↔ ∀ s ∈ S, Set.MapsTo f s t

@[simp]

theorem Set.mapsTo_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : Set β} {f : α → β} :

Set.MapsTo f (⋃ (i : ι), s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t

theorem Set.mapsTo_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set β} {f : α → β} :

Set.MapsTo f (⋃ (i : ι), ⋃ (j : κ i), s i j) t ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t

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

Set.MapsTo f (⋃ (i : ι), s i) (⋃ (i : ι), t i)

theorem Set.mapsTo_iUnion₂_iUnion₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ 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)

@[simp]

theorem Set.mapsTo_sInter {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β} :

Set.MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, Set.MapsTo f s t

@[simp]

theorem Set.mapsTo_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ι → Set β} {f : α → β} :

Set.MapsTo f s (⋂ (i : ι), t i) ↔ ∀ (i : ι), Set.MapsTo f s (t i)

theorem Set.mapsTo_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β} :

Set.MapsTo f s (⋂ (i : ι), ⋂ (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)

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

Set.MapsTo f (⋂ (i : ι), s i) (⋂ (i : ι), t i)

theorem Set.mapsTo_iInter₂_iInter₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ 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 ∈ 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 : Set α) => 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 ∈ 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 : Set α) => 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 : Set α) => 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 ∈ s, {f i}

theorem Set.biUnion_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β} :

⋃ 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 ∈ 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 ∈ f '' s, g x = ⋃ y ∈ s, g (f y)

theorem Set.biInter_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β} :

⋂ x ∈ f '' s, g x = ⋂ 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 ∈ 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 ∈ s, f ⁻¹' t

@[simp]

theorem Set.biUnion_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) :

⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

theorem Set.biUnion_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : α → β) :

⋃ 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 : Set β) => s ×ˢ t) '' C)

theorem Set.iUnion_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : Set β} :

(⋃ (i : ι), s i) ×ˢ t = ⋃ (i : ι), s i ×ˢ t

theorem Set.iUnion₂_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ 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 : Set α) => s ×ˢ t) '' C)

theorem Set.iUnion_prod {ι : Type u_11} {ι' : Type u_12} {α : Type u_13} {β : Type u_14} (s : ι → Set α) (t : ι' → Set β) :

⋃ (x : ι × ι'), s x.1 ×ˢ t x.2 = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i

theorem Set.iUnion_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γ → Set α) :

⋃ (x : β × γ), f x = ⋃ (i : β), ⋃ (j : γ), f (i, j)

Analogue of iSup_prod for sets.

theorem Set.iUnion_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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 ∈ S ×ˢ T, r.1 ×ˢ r.2

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 ∈ S ×ˢ T, r.1 ×ˢ r.2

theorem Set.sInter_prod {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : Set.Nonempty S) (t : Set β) :

⋂₀ S ×ˢ t = ⋂ 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 ∈ T, s ×ˢ t

theorem Set.prod_iInter {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :

s ×ˢ ⋂ (i : ι), t i = ⋂ (i : ι), s ×ˢ t i

theorem Set.image2_eq_iUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β) :

Set.image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

The Set.image2 version of Set.image_eq_iUnion

theorem Set.iUnion_image_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β} :

⋃ 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 ∈ t, (fun (x : α) => f x b) '' s = Set.image2 f s t

theorem Set.image2_iUnion_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : ι → Set α) (t : Set β) :

Set.image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), Set.image2 f (s i) t

theorem Set.image2_iUnion_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : Set α) (t : ι → Set β) :

Set.image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), Set.image2 f s (t i)

theorem Set.image2_iUnion₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ) (s : (i : ι) → κ 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.prod_eq_biUnion_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :

s ×ˢ t = ⋃ 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 ∈ t, (fun (a : α) => (a, b)) '' s

theorem Set.seq_def {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} :

Set.seq s t = ⋃ f ∈ s, f '' t

theorem Set.seq_subset {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α} {u : Set β} :

Set.seq s t ⊆ u ↔ ∀ f ∈ s, ∀ 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 : α → β) => f ∘ x) '' 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 ∈ 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 ∈ i, Function.eval a ⁻¹' (s a \ t a)

theorem Set.iUnion_univ_pi {α : Type u_1} {π : α → Type u_11} {ι : α → Type u_12} (t : (a : α) → ι a → Set (π a)) :

(⋃ (x : (a : α) → ι a), Set.pi Set.univ fun (a : α) => t a (x a)) = Set.pi Set.univ fun (a : α) => ⋃ (j : ι a), t a 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 ∈ S, Disjoint s t

@[simp]

theorem Set.disjoint_sUnion_right {α : Type u_1} {s : Set α} {S : Set (Set α)} :

Disjoint s (⋃₀ S) ↔ ∀ 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 ∈ s, Set.Ici a

theorem Set.Iic_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) :

Set.Iic (sInf s) = ⋂ a ∈ s, Set.Iic a

theorem Set.biUnion_diff_biUnion_subset {α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ : Set α) (s₂ : Set α) :

(⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t 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.

Equations

Set.sigmaToiUnion t x = { val := ↑x.snd, property := (_ : ↑x.snd ∈ ⋃ (i : α), t i) }

Instances For

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 : Pairwise fun (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 : Pairwise fun (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 : Pairwise fun (i j : α) => Disjoint (t i) (t j)) :

↑(⋃ (i : α), t i) ≃ (i : α) × ↑(t i)

Equivalence between a disjoint union and a dependent sum.

Equations

Set.unionEqSigmaOfDisjoint h = (Equiv.ofBijective (Set.sigmaToiUnion t) (_ : Function.Bijective (Set.sigmaToiUnion t))).symm

Instances For

theorem Set.iUnion_ge_eq_iUnion_nat_add {α : Type u_1} (u : ℕ → Set α) (n : ℕ) :

⋃ (i : ℕ), ⋃ (_ : i ≥ n), u i = ⋃ (i : ℕ), u (i + n)

theorem Set.iInter_ge_eq_iInter_nat_add {α : Type u_1} (u : ℕ → Set α) (n : ℕ) :

⋂ (i : ℕ), ⋂ (_ : i ≥ n), u i = ⋂ (i : ℕ), u (i + n)

theorem Monotone.iUnion_nat_add {α : Type u_1} {f : ℕ → Set α} (hf : 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 ∈ ⋃ (i : ι), s i, f a = ⨆ (i : ι), ⨆ a ∈ s i, f a

theorem iInf_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice β] (s : ι → Set α) (f : α → β) :

⨅ a ∈ ⋃ (i : ι), s i, f a = ⨅ (i : ι), ⨅ a ∈ s i, f a

theorem sSup_iUnion {β : Type u_2} {ι : Sort u_4} [CompleteLattice β] (t : ι → Set β) :

sSup (⋃ (i : ι), t i) = ⨆ (i : ι), sSup (t i)

theorem sSup_sUnion {β : Type u_2} [CompleteLattice β] (s : Set (Set β)) :

sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

theorem sInf_sUnion {β : Type u_2} [CompleteLattice β] (s : Set (Set β)) :

sInf (⋃₀ s) = ⨅ t ∈ s, sInf t

theorem iSup_sUnion {α : Type u_1} {β : Type u_2} [CompleteLattice β] (S : Set (Set α)) (f : α → β) :

⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x

theorem iInf_sUnion {α : Type u_1} {β : Type u_2} [CompleteLattice β] (S : Set (Set α)) (f : α → β) :

⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x

theorem forall_sUnion {α : Type u_1} {S : Set (Set α)} {p : α → Prop} :

(∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x