Documentation

instance Set.instInfSetSet {α : Type u_1} :

InfSet (Set α)

Equations

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

instance Set.instSupSetSet {α : Type u_1} :

SupSet (Set α)

Equations

Set.instSupSetSet = { sSup := fun s => {a | ∃ t, 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 : 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

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⋃_,_» :

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 :

Equations

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

Instances For

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

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, 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, 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, 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, s i j

instance Set.Set.completeAtomicBooleanAlgebra {α : Type u_1} :

CompleteAtomicBooleanAlgebra (Set α)

Equations

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

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.

Equations

Set.kernImage f s = {y | ∀ ⦃x : α⦄, f x = y → x ∈ s}

Instances For

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

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

theorem Set.iUnion_plift_down {α : Type u_1} {ι : Sort u_4} (f : ι → Set α) :

⋃ i, f i.down = ⋃ i, f i

theorem Set.iInter_plift_up {α : Type u_1} {ι : Sort u_4} (f : PLift ι → Set α) :

⋂ i, f { down := i } = ⋂ i, f i

theorem Set.iInter_plift_down {α : Type u_1} {ι : Sort u_4} (f : ι → Set α) :

⋂ i, f i.down = ⋂ i, f i

theorem Set.iUnion_eq_if {α : Type u_1} {p : Prop} [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, 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, 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, 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, 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, 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', 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, 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, 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, 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, s i j ⊆ ⋃ i, ⋃ j, 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, s i j ⊆ ⋂ i, ⋂ j, 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, s i j ⊆ ⋃ i', ⋃ j', 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, s i j ⊆ ⋂ i', ⋂ j', t i' j'

theorem Set.iUnion₂_subset_iUnion {α : Type u_1} {ι : Sort u_4} (κ : ι → Sort u_11) (s : ι → Set α) :

⋃ i, ⋃ x, 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, 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, s i j = ⋃ i, ⋃ j, 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, s i j = ⋂ i, ⋂ j, 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, s i j)ᶜ = ⋂ i, ⋂ j, (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, s i j)ᶜ = ⋃ i, ⋃ j, (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, s o = s none ∪ ⋃ i, s (some i)

theorem Set.iInter_option {α : Type u_1} {ι : Type u_11} (s : Option ι → Set α) :

⋂ o, 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 => 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 ∈ 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₂, ⋃ j₂, s i₁ j₁ i₂ j₂ = ⋃ i₂, ⋃ j₂, ⋃ i₁, ⋃ j₁, 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₂, ⋂ j₂, s i₁ j₁ i₂ j₂ = ⋂ i₂, ⋂ j₂, ⋂ i₁, ⋂ j₁, 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 : α), 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 : α), 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 : α), 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, 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, t ↑x (_ : ↑x ∈ s)

theorem Set.iUnion_subtype {α : Type u_1} {β : Type u_2} (p : α → Prop) (s : { x // p x } → Set β) :

⋃ 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, 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, 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, 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, t i j = ⋃ i, ⋃ j, 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, s i j) ∩ t = ⋃ i, ⋃ j, 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, t i j = ⋂ i, ⋂ j, 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, s i j) ∪ t = ⋂ i, ⋂ j, 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.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' : 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.

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 ∈ 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, 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, 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, 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, {↑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, ↑i

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

⋂₀ s = ⋂ i, ↑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, bif b then s₁ else s₂

theorem Set.inter_eq_iInter {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :

s₁ ∩ s₂ = ⋂ b, 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 => ↑(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, t i j = ⋂ i, ⋂ j, 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, s i j) ∪ t = ⋂ i, ⋂ j, 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, 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, s i j) (⋃ i, ⋃ j, 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, 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, s i j) (⋂ i, ⋂ j, 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, s i j ⊆ ⋂ i, ⋂ j, 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, s i j = ⋂ i, ⋂ j, 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, 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, s i j) (⋃ i, ⋃ j, 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, s i j = ⋃ i, ⋃ j, 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, s i j = ⋃ i, ⋃ j, 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, s i j = ⋂ i, ⋂ j, 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, t i j = ⋃ i, ⋃ j, 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, s i j) ×ˢ t = ⋃ i, ⋃ j, 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.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.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 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, s i j) t = ⋃ i, ⋃ j, 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, t i j) = ⋃ i, ⋃ j, 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, s i j) t ⊆ ⋂ i, ⋂ j, 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, t i j) ⊆ ⋂ i, ⋂ j, 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 ∈ s, ⋃ 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 ∈ 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

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.

Equations

Set.seq s t = {b | ∃ f, f ∈ s ∧ ∃ a, a ∈ t ∧ f a = b}

Instances For

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

Set.seq s t = ⋃ 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 ∈ 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} {ι : 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, 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, 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, f i j) = ⋂ i, ⋂ j, 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, f i j) = ⋂ i, ⋂ j, 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 : ∀ (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.

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_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 : α), x ∈ ⋃₀ S → p x) ↔ ∀ (s : Set α), s ∈ S → ∀ (x : α), x ∈ s → p x