# Documentation

Mathlib.Data.Set.Lattice

# The set lattice #

This file provides usual set notation for unions and intersections, a CompleteLattice instance for Set α, and some more set constructions.

## Main declarations #

• Set.unionᵢ: indexed union. Union of an indexed family of sets.
• Set.interᵢ: indexed intersection. Intersection of an indexed family of sets.
• Set.interₛ: set intersection. Intersection of sets belonging to a set of sets.
• Set.unionₛ: set union. Union of sets belonging to a set of sets.
• Set.interₛ_eq_binterᵢ, Set.unionₛ_eq_binterᵢ: Shows that ⋂₀ s = ⋂ x ∈ s, x⋂₀ s = ⋂ x ∈ s, x⋂ x ∈ s, x∈ s, x and ⋃₀ s = ⋃ x ∈ s, x⋃₀ s = ⋃ x ∈ s, x⋃ x ∈ s, x∈ s, x.
• Set.completeBooleanAlgebra: Set α is a CompleteBooleanAlgebra with ≤ = ⊆≤ = ⊆⊆, < = ⊂⊂, ⊓ = ∩⊓ = ∩∩, ⊔ = ∪⊔ = ∪∪, ⨅ = ⋂⨅ = ⋂⋂, ⨆ = ⋃⨆ = ⋃⋃ and \ as the set difference. See Set.BooleanAlgebra.
• Set.kern_image: For a function f : α → β→ β, s.kern_image f is the set of y such that f ⁻¹ y ⊆ s⁻¹ y ⊆ s⊆ s.
• Set.seq: Union of the image of a set under a sequence of functions. seq s t is the union of f '' t over all f ∈ s∈ s, where t : Set α and s : Set (α → β)→ β).
• Set.unionᵢ_eq_sigma_of_disjoint: Equivalence between ⋃ i, t i⋃ i, t i and Σ i, t i, where t is an indexed family of disjoint sets.

## Naming convention #

In lemma names,

• ⋃ i, s i⋃ i, s i is called unionᵢ
• ⋂ i, s i⋂ i, s i is called interᵢ
• ⋃ i j, s i j⋃ i j, s i j is called unionᵢ₂. This is a unionᵢ inside a unionᵢ.
• ⋂ i j, s i j⋂ i j, s i j is called interᵢ₂. This is an interᵢ inside an interᵢ.
• ⋃ i ∈ s, t i⋃ i ∈ s, t i∈ s, t i is called bunionᵢ for "bounded unionᵢ". This is the special case of unionᵢ₂ where j : i ∈ s∈ s.
• ⋂ i ∈ s, t i⋂ i ∈ s, t i∈ s, t i is called binterᵢ for "bounded interᵢ". This is the special case of interᵢ₂ where j : i ∈ s∈ s.

## Notation #

• ⋃⋃: Set.unionᵢ
• ⋂⋂: Set.interᵢ
• ⋃₀⋃₀: Set.unionₛ
• ⋂₀⋂₀: Set.interₛ

### Complete lattice and complete Boolean algebra instances #

instance Set.instInfSetSet {α : Type u_1} :
InfSet (Set α)
Equations
• Set.instInfSetSet = { infₛ := fun s => { a | ∀ (t : Set α), t sa t } }
instance Set.instSupSetSet {α : Type u_1} :
SupSet (Set α)
Equations
• Set.instSupSetSet = { supₛ := fun s => { a | t, t s a t } }
def Set.interₛ {α : Type u_1} (S : Set (Set α)) :
Set α

Intersection of a set of sets.

Equations

Notation for Set.interₛ Intersection of a set of sets.

Equations
def Set.unionₛ {α : Type u_1} (S : Set (Set α)) :
Set α

Intersection of a set of sets.

Equations

Notation for Set.unionₛ. Union of a set of sets.

Equations
@[simp]
theorem Set.mem_interₛ {α : Type u_1} {x : α} {S : Set (Set α)} :
x ⋂₀ S ∀ (t : Set α), t Sx t
@[simp]
theorem Set.mem_unionₛ {α : Type u_1} {x : α} {S : Set (Set α)} :
x ⋃₀ S t, t S x t
def Set.unionᵢ {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
Set β

Indexed union of a family of sets

Equations
def Set.interᵢ {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
Set β

Indexed intersection of a family of sets

Equations

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

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

Notation for Set.interᵢ. Indexed intersection of a family of sets

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Set.supₛ_eq_unionₛ {α : Type u_1} (S : Set (Set α)) :
@[simp]
theorem Set.infₛ_eq_interₛ {α : Type u_1} (S : Set (Set α)) :
@[simp]
theorem Set.supᵢ_eq_unionᵢ {α : Type u_1} {ι : Sort u_2} (s : ιSet α) :
@[simp]
theorem Set.infᵢ_eq_interᵢ {α : Type u_1} {ι : Sort u_2} (s : ιSet α) :
@[simp]
theorem Set.mem_unionᵢ {α : Type u_1} {ι : Sort u_2} {x : α} {s : ιSet α} :
(x Set.unionᵢ fun i => s i) i, x s i
@[simp]
theorem Set.mem_interᵢ {α : Type u_1} {ι : Sort u_2} {x : α} {s : ιSet α} :
(x Set.interᵢ fun i => s i) ∀ (i : ι), x s i
theorem Set.mem_unionᵢ₂ {γ : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {x : γ} {s : (i : ι) → κ iSet γ} :
(x Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) i j, x s i j
theorem Set.mem_interᵢ₂ {γ : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {x : γ} {s : (i : ι) → κ iSet γ} :
(x Set.interᵢ fun i => Set.interᵢ fun j => s i j) ∀ (i : ι) (j : κ i), x s i j
theorem Set.mem_unionᵢ_of_mem {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {a : α} (i : ι) (ha : a s i) :
a Set.unionᵢ fun i => s i
theorem Set.mem_unionᵢ₂_of_mem {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {a : α} {i : ι} (j : κ i) (ha : a s i j) :
a Set.unionᵢ fun i => Set.unionᵢ fun j => s i j
theorem Set.mem_interᵢ_of_mem {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {a : α} (h : ∀ (i : ι), a s i) :
a Set.interᵢ fun i => s i
theorem Set.mem_interᵢ₂_of_mem {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {a : α} (h : ∀ (i : ι) (j : κ i), a s i j) :
a Set.interᵢ fun i => Set.interᵢ fun j => s i j
Equations
• One or more equations did not get rendered due to their size.
theorem Set.image_preimage {α : Type u_1} {β : Type u_2} {f : αβ} :
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⁻¹ y ⊆ s⊆ s.

Equations
• = { y | ∀ ⦃x : α⦄, f x = yx s }
theorem Set.preimage_kernImage {α : Type u_2} {β : Type u_1} {f : αβ} :

### Union and intersection over an indexed family of sets #

instance Set.instOrderTopSetInstLESet {α : Type u_1} :
Equations
theorem Set.unionᵢ_congr_Prop {α : Type u_1} {p : Prop} {q : Prop} {f₁ : pSet α} {f₂ : qSet α} (pq : p q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) :
=
theorem Set.interᵢ_congr_Prop {α : Type u_1} {p : Prop} {q : Prop} {f₁ : pSet α} {f₂ : qSet α} (pq : p q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) :
=
theorem Set.unionᵢ_plift_up {α : Type u_2} {ι : Sort u_1} (f : Set α) :
(Set.unionᵢ fun i => f { down := i }) = Set.unionᵢ fun i => f i
theorem Set.unionᵢ_plift_down {α : Type u_1} {ι : Sort u_2} (f : ιSet α) :
(Set.unionᵢ fun i => f i.down) = Set.unionᵢ fun i => f i
theorem Set.interᵢ_plift_up {α : Type u_2} {ι : Sort u_1} (f : Set α) :
(Set.interᵢ fun i => f { down := i }) = Set.interᵢ fun i => f i
theorem Set.interᵢ_plift_down {α : Type u_1} {ι : Sort u_2} (f : ιSet α) :
(Set.interᵢ fun i => f i.down) = Set.interᵢ fun i => f i
theorem Set.unionᵢ_eq_if {α : Type u_1} {p : Prop} [inst : ] (s : Set α) :
(Set.unionᵢ fun _h => s) = if p then s else
theorem Set.unionᵢ_eq_dif {α : Type u_1} {p : Prop} [inst : ] (s : pSet α) :
(Set.unionᵢ fun h => s h) = if h : p then s h else
theorem Set.interᵢ_eq_if {α : Type u_1} {p : Prop} [inst : ] (s : Set α) :
(Set.interᵢ fun _h => s) = if p then s else Set.univ
theorem Set.infᵢ_eq_dif {α : Type u_1} {p : Prop} [inst : ] (s : pSet α) :
(Set.interᵢ fun h => 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_1} (t : Set ι) (s : ιSet β) (w : (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) = ) (x : β) :
i, i t x s i
theorem Set.nonempty_of_union_eq_top_of_nonempty {α : Type u_2} {ι : Type u_1} (t : Set ι) (s : ιSet α) (H : ) (w : (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) = ) :
theorem Set.setOf_exists {β : Type u_1} {ι : Sort u_2} (p : ιβProp) :
{ x | i, p i x } = Set.unionᵢ fun i => { x | p i x }
theorem Set.setOf_forall {β : Type u_1} {ι : Sort u_2} (p : ιβProp) :
{ x | (i : ι) → p i x } = Set.interᵢ fun i => { x | p i x }
theorem Set.unionᵢ_subset {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : Set α} (h : ∀ (i : ι), s i t) :
(Set.unionᵢ fun i => s i) t
theorem Set.unionᵢ₂_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : Set α} (h : ∀ (i : ι) (j : κ i), s i j t) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t
theorem Set.subset_interᵢ {β : Type u_1} {ι : Sort u_2} {t : Set β} {s : ιSet β} (h : ∀ (i : ι), t s i) :
t Set.interᵢ fun i => s i
theorem Set.subset_interᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : Set α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s t i j) :
s Set.interᵢ fun i => Set.interᵢ fun j => t i j
@[simp]
theorem Set.unionᵢ_subset_iff {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : Set α} :
(Set.unionᵢ fun i => s i) t ∀ (i : ι), s i t
theorem Set.unionᵢ₂_subset_iff {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : Set α} :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t ∀ (i : ι) (j : κ i), s i j t
@[simp]
theorem Set.subset_interᵢ_iff {α : Type u_1} {ι : Sort u_2} {s : Set α} {t : ιSet α} :
(s Set.interᵢ fun i => t i) ∀ (i : ι), s t i
theorem Set.subset_interᵢ₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : Set α} {t : (i : ι) → κ iSet α} :
(s Set.interᵢ fun i => Set.interᵢ fun j => t i j) ∀ (i : ι) (j : κ i), s t i j
theorem Set.subset_unionᵢ {β : Type u_1} {ι : Sort u_2} (s : ιSet β) (i : ι) :
s i Set.unionᵢ fun i => s i
theorem Set.interᵢ_subset {β : Type u_1} {ι : Sort u_2} (s : ιSet β) (i : ι) :
(Set.interᵢ fun i => s i) s i
theorem Set.subset_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} (i : ι) (j : κ i) :
s i j Set.unionᵢ fun i' => Set.unionᵢ fun j' => s i' j'
theorem Set.interᵢ₂_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} (i : ι) (j : κ i) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) s i j
theorem Set.subset_unionᵢ_of_subset {α : Type u_1} {ι : Sort u_2} {s : Set α} {t : ιSet α} (i : ι) (h : s t i) :
s Set.unionᵢ fun i => t i

This rather trivial consequence of subset_unionᵢis convenient with apply, and has i explicit for this purpose.

theorem Set.interᵢ_subset_of_subset {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : Set α} (i : ι) (h : s i t) :
(Set.interᵢ fun i => s i) t

This rather trivial consequence of interᵢ_subsetis convenient with apply, and has i explicit for this purpose.

theorem Set.subset_unionᵢ₂_of_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : Set α} {t : (i : ι) → κ iSet α} (i : ι) (j : κ i) (h : s t i j) :
s Set.unionᵢ fun i => Set.unionᵢ fun j => t i j

This rather trivial consequence of subset_unionᵢ₂ is convenient with apply, and has i and j explicit for this purpose.

theorem Set.interᵢ₂_subset_of_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : Set α} (i : ι) (j : κ i) (h : s i j t) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) t

This rather trivial consequence of interᵢ₂_subset is convenient with apply, and has i and j explicit for this purpose.

theorem Set.unionᵢ_mono {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i t i) :
(Set.unionᵢ fun i => s i) Set.unionᵢ fun i => t i
theorem Set.unionᵢ₂_mono {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j t i j) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) Set.unionᵢ fun i => Set.unionᵢ fun j => t i j
theorem Set.interᵢ_mono {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i t i) :
(Set.interᵢ fun i => s i) Set.interᵢ fun i => t i
theorem Set.interᵢ₂_mono {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j t i j) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) Set.interᵢ fun i => Set.interᵢ fun j => t i j
theorem Set.unionᵢ_mono' {α : Type u_1} {ι : Sort u_3} {ι₂ : Sort u_2} {s : ιSet α} {t : ι₂Set α} (h : ∀ (i : ι), j, s i t j) :
(Set.unionᵢ fun i => s i) Set.unionᵢ fun i => t i
theorem Set.unionᵢ₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_2} {κ : ιSort u_5} {κ' : ι'Sort u_3} {s : (i : ι) → κ iSet α} {t : (i' : ι') → κ' i'Set α} (h : ∀ (i : ι) (j : κ i), i' j', s i j t i' j') :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) Set.unionᵢ fun i' => Set.unionᵢ fun j' => t i' j'
theorem Set.interᵢ_mono' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {s : ιSet α} {t : ι'Set α} (h : ∀ (j : ι'), i, s i t j) :
(Set.interᵢ fun i => s i) Set.interᵢ fun j => t j
theorem Set.interᵢ₂_mono' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_4} {κ : ιSort u_3} {κ' : ι'Sort u_5} {s : (i : ι) → κ iSet α} {t : (i' : ι') → κ' i'Set α} (h : ∀ (i' : ι') (j' : κ' i'), i j, s i j t i' j') :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) Set.interᵢ fun i' => Set.interᵢ fun j' => t i' j'
theorem Set.unionᵢ₂_subset_unionᵢ {α : Type u_2} {ι : Sort u_3} (κ : ιSort u_1) (s : ιSet α) :
(Set.unionᵢ fun i => Set.unionᵢ fun _j => s i) Set.unionᵢ fun i => s i
theorem Set.interᵢ_subset_interᵢ₂ {α : Type u_2} {ι : Sort u_3} (κ : ιSort u_1) (s : ιSet α) :
(Set.interᵢ fun i => s i) Set.interᵢ fun i => Set.interᵢ fun _j => s i
theorem Set.unionᵢ_setOf {α : Type u_1} {ι : Sort u_2} (P : ιαProp) :
(Set.unionᵢ fun i => { x | P i x }) = { x | i, P i x }
theorem Set.interᵢ_setOf {α : Type u_1} {ι : Sort u_2} (P : ιαProp) :
(Set.interᵢ fun i => { x | P i x }) = { x | (i : ι) → P i x }
theorem Set.unionᵢ_congr_of_surjective {α : Type u_1} {ι : Sort u_2} {ι₂ : Sort u_3} {f : ιSet α} {g : ι₂Set α} (h : ιι₂) (h1 : ) (h2 : ∀ (x : ι), g (h x) = f x) :
(Set.unionᵢ fun x => f x) = Set.unionᵢ fun y => g y
theorem Set.interᵢ_congr_of_surjective {α : Type u_1} {ι : Sort u_2} {ι₂ : Sort u_3} {f : ιSet α} {g : ι₂Set α} (h : ιι₂) (h1 : ) (h2 : ∀ (x : ι), g (h x) = f x) :
(Set.interᵢ fun x => f x) = Set.interᵢ fun y => g y
theorem Set.unionᵢ_congr {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i = t i) :
(Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => t i
theorem Set.interᵢ_congr {α : Type u_1} {ι : Sort u_2} {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i = t i) :
(Set.interᵢ fun i => s i) = Set.interᵢ fun i => t i
theorem Set.unionᵢ₂_congr {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j = t i j) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => t i j
theorem Set.interᵢ₂_congr {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet α} (h : ∀ (i : ι) (j : κ i), s i j = t i j) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) = Set.interᵢ fun i => Set.interᵢ fun j => t i j
theorem Set.unionᵢ_const {β : Type u_1} {ι : Sort u_2} [inst : ] (s : Set β) :
(Set.unionᵢ fun _i => s) = s
theorem Set.interᵢ_const {β : Type u_1} {ι : Sort u_2} [inst : ] (s : Set β) :
(Set.interᵢ fun _i => s) = s
theorem Set.unionᵢ_eq_const {α : Type u_1} {ι : Sort u_2} [inst : ] {f : ιSet α} {s : Set α} (hf : ∀ (i : ι), f i = s) :
(Set.unionᵢ fun i => f i) = s
theorem Set.interᵢ_eq_const {α : Type u_1} {ι : Sort u_2} [inst : ] {f : ιSet α} {s : Set α} (hf : ∀ (i : ι), f i = s) :
(Set.interᵢ fun i => f i) = s
@[simp]
theorem Set.compl_unionᵢ {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
(Set.unionᵢ fun i => s i) = Set.interᵢ fun i => s i
theorem Set.compl_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : (i : ι) → κ iSet α) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.interᵢ fun i => Set.interᵢ fun j => s i j
@[simp]
theorem Set.compl_interᵢ {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
(Set.interᵢ fun i => s i) = Set.unionᵢ fun i => s i
theorem Set.compl_interᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : (i : ι) → κ iSet α) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j
theorem Set.unionᵢ_eq_compl_interᵢ_compl {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
(Set.unionᵢ fun i => s i) = (Set.interᵢ fun i => s i)
theorem Set.interᵢ_eq_compl_unionᵢ_compl {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
(Set.interᵢ fun i => s i) = (Set.unionᵢ fun i => s i)
theorem Set.inter_unionᵢ {β : Type u_1} {ι : Sort u_2} (s : Set β) (t : ιSet β) :
(s Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s t i
theorem Set.unionᵢ_inter {β : Type u_1} {ι : Sort u_2} (s : Set β) (t : ιSet β) :
(Set.unionᵢ fun i => t i) s = Set.unionᵢ fun i => t i s
theorem Set.unionᵢ_union_distrib {β : Type u_1} {ι : Sort u_2} (s : ιSet β) (t : ιSet β) :
(Set.unionᵢ fun i => s i t i) = (Set.unionᵢ fun i => s i) Set.unionᵢ fun i => t i
theorem Set.interᵢ_inter_distrib {β : Type u_1} {ι : Sort u_2} (s : ιSet β) (t : ιSet β) :
(Set.interᵢ fun i => s i t i) = (Set.interᵢ fun i => s i) Set.interᵢ fun i => t i
theorem Set.union_unionᵢ {β : Type u_2} {ι : Sort u_1} [inst : ] (s : Set β) (t : ιSet β) :
(s Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s t i
theorem Set.unionᵢ_union {β : Type u_2} {ι : Sort u_1} [inst : ] (s : Set β) (t : ιSet β) :
(Set.unionᵢ fun i => t i) s = Set.unionᵢ fun i => t i s
theorem Set.inter_interᵢ {β : Type u_2} {ι : Sort u_1} [inst : ] (s : Set β) (t : ιSet β) :
(s Set.interᵢ fun i => t i) = Set.interᵢ fun i => s t i
theorem Set.interᵢ_inter {β : Type u_2} {ι : Sort u_1} [inst : ] (s : Set β) (t : ιSet β) :
(Set.interᵢ fun i => t i) s = Set.interᵢ fun i => t i s
theorem Set.union_interᵢ {β : Type u_1} {ι : Sort u_2} (s : Set β) (t : ιSet β) :
(s Set.interᵢ fun i => t i) = Set.interᵢ fun i => s t i
theorem Set.interᵢ_union {β : Type u_1} {ι : Sort u_2} (s : ιSet β) (t : Set β) :
(Set.interᵢ fun i => s i) t = Set.interᵢ fun i => s i t
theorem Set.unionᵢ_diff {β : Type u_1} {ι : Sort u_2} (s : Set β) (t : ιSet β) :
(Set.unionᵢ fun i => t i) \ s = Set.unionᵢ fun i => t i \ s
theorem Set.diff_unionᵢ {β : Type u_2} {ι : Sort u_1} [inst : ] (s : Set β) (t : ιSet β) :
(s \ Set.unionᵢ fun i => t i) = Set.interᵢ fun i => s \ t i
theorem Set.diff_interᵢ {β : Type u_1} {ι : Sort u_2} (s : Set β) (t : ιSet β) :
(s \ Set.interᵢ fun i => t i) = Set.unionᵢ fun i => s \ t i
theorem Set.directed_on_unionᵢ {α : Type u_1} {ι : Sort u_2} {r : ααProp} {f : ιSet α} (hd : Directed (fun x x_1 => x x_1) f) (h : ∀ (x : ι), DirectedOn r (f x)) :
DirectedOn r (Set.unionᵢ fun x => f x)
theorem Set.unionᵢ_inter_subset {ι : Sort u_1} {α : Type u_2} {s : ιSet α} {t : ιSet α} :
(Set.unionᵢ fun i => s i t i) (Set.unionᵢ fun i => s i) Set.unionᵢ fun i => t i
theorem Set.unionᵢ_inter_of_monotone {ι : Type u_1} {α : Type u_2} [inst : ] [inst : IsDirected ι fun x x_1 => x x_1] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
(Set.unionᵢ fun i => s i t i) = (Set.unionᵢ fun i => s i) Set.unionᵢ fun i => t i
theorem Set.unionᵢ_inter_of_antitone {ι : Type u_1} {α : Type u_2} [inst : ] [inst : IsDirected ι (Function.swap fun x x_1 => x x_1)] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
(Set.unionᵢ fun i => s i t i) = (Set.unionᵢ fun i => s i) Set.unionᵢ fun i => t i
theorem Set.interᵢ_union_of_monotone {ι : Type u_1} {α : Type u_2} [inst : ] [inst : IsDirected ι (Function.swap fun x x_1 => x x_1)] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
(Set.interᵢ fun i => s i t i) = (Set.interᵢ fun i => s i) Set.interᵢ fun i => t i
theorem Set.interᵢ_union_of_antitone {ι : Type u_1} {α : Type u_2} [inst : ] [inst : IsDirected ι fun x x_1 => x x_1] {s : ιSet α} {t : ιSet α} (hs : ) (ht : ) :
(Set.interᵢ fun i => s i t i) = (Set.interᵢ fun i => s i) Set.interᵢ fun i => t i
theorem Set.unionᵢ_interᵢ_subset {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_2} {s : ιι'Set α} :
(Set.unionᵢ fun j => Set.interᵢ fun i => s i j) Set.interᵢ fun i => Set.unionᵢ fun j => s i j

An equality version of this lemma is unionᵢ_interᵢ_of_monotone in Data.Set.Finite.

theorem Set.unionᵢ_option {α : Type u_2} {ι : Type u_1} (s : Set α) :
(Set.unionᵢ fun o => s o) = s none Set.unionᵢ fun i => s (some i)
theorem Set.interᵢ_option {α : Type u_2} {ι : Type u_1} (s : Set α) :
(Set.interᵢ fun o => s o) = s none Set.interᵢ fun i => s (some i)
theorem Set.unionᵢ_dite {α : Type u_1} {ι : Sort u_2} (p : ιProp) [inst : ] (f : (i : ι) → p iSet α) (g : (i : ι) → ¬p iSet α) :
(Set.unionᵢ fun i => if h : p i then f i h else g i h) = (Set.unionᵢ fun i => Set.unionᵢ fun h => f i h) Set.unionᵢ fun i => Set.unionᵢ fun h => g i h
theorem Set.unionᵢ_ite {α : Type u_1} {ι : Sort u_2} (p : ιProp) [inst : ] (f : ιSet α) (g : ιSet α) :
(Set.unionᵢ fun i => if p i then f i else g i) = (Set.unionᵢ fun i => Set.unionᵢ fun _h => f i) Set.unionᵢ fun i => Set.unionᵢ fun _h => g i
theorem Set.interᵢ_dite {α : Type u_1} {ι : Sort u_2} (p : ιProp) [inst : ] (f : (i : ι) → p iSet α) (g : (i : ι) → ¬p iSet α) :
(Set.interᵢ fun i => if h : p i then f i h else g i h) = (Set.interᵢ fun i => Set.interᵢ fun h => f i h) Set.interᵢ fun i => Set.interᵢ fun h => g i h
theorem Set.interᵢ_ite {α : Type u_1} {ι : Sort u_2} (p : ιProp) [inst : ] (f : ιSet α) (g : ιSet α) :
(Set.interᵢ fun i => if p i then f i else g i) = (Set.interᵢ fun i => Set.interᵢ fun _h => f i) Set.interᵢ fun i => Set.interᵢ fun _h => g i
theorem Set.image_projection_prod {ι : Type u_1} {α : ιType u_2} {v : (i : ι) → Set (α i)} (hv : Set.Nonempty (Set.pi Set.univ v)) (i : ι) :
((fun x => x i) '' Set.interᵢ fun k => (fun x => x k) ⁻¹' v k) = v i

### Unions and intersections indexed by Prop#

theorem Set.interᵢ_false {α : Type u_1} {s : FalseSet α} :
= Set.univ
theorem Set.unionᵢ_false {α : Type u_1} {s : FalseSet α} :
@[simp]
theorem Set.interᵢ_true {α : Type u_1} {s : TrueSet α} :
@[simp]
theorem Set.unionᵢ_true {α : Type u_1} {s : TrueSet α} :
@[simp]
theorem Set.interᵢ_exists {α : Type u_2} {ι : Sort u_1} {p : ιProp} {f : Set α} :
(Set.interᵢ fun x => f x) = Set.interᵢ fun i => Set.interᵢ fun h => f (_ : )
@[simp]
theorem Set.unionᵢ_exists {α : Type u_2} {ι : Sort u_1} {p : ιProp} {f : Set α} :
(Set.unionᵢ fun x => f x) = Set.unionᵢ fun i => Set.unionᵢ fun h => f (_ : )
@[simp]
theorem Set.unionᵢ_empty {α : Type u_1} {ι : Sort u_2} :
(Set.unionᵢ fun _i => ) =
@[simp]
theorem Set.interᵢ_univ {α : Type u_1} {ι : Sort u_2} :
(Set.interᵢ fun _i => Set.univ) = Set.univ
@[simp]
theorem Set.unionᵢ_eq_empty {α : Type u_1} {ι : Sort u_2} {s : ιSet α} :
(Set.unionᵢ fun i => s i) = ∀ (i : ι), s i =
@[simp]
theorem Set.interᵢ_eq_univ {α : Type u_1} {ι : Sort u_2} {s : ιSet α} :
(Set.interᵢ fun i => s i) = Set.univ ∀ (i : ι), s i = Set.univ
@[simp]
theorem Set.nonempty_unionᵢ {α : Type u_1} {ι : Sort u_2} {s : ιSet α} :
Set.Nonempty (Set.unionᵢ fun i => s i) i, Set.Nonempty (s i)
theorem Set.nonempty_bunionᵢ {α : Type u_1} {β : Type u_2} {t : Set α} {s : αSet β} :
Set.Nonempty (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) i, i t Set.Nonempty (s i)
theorem Set.unionᵢ_nonempty_index {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
(Set.unionᵢ fun h => t h) = Set.unionᵢ fun x => Set.unionᵢ fun h => t (_ : x, x s)
@[simp]
theorem Set.interᵢ_interᵢ_eq_left {α : Type u_2} {β : Type u_1} {b : β} {s : (x : β) → x = bSet α} :
(Set.interᵢ fun x => Set.interᵢ fun h => s x h) = s b (_ : b = b)
@[simp]
theorem Set.interᵢ_interᵢ_eq_right {α : Type u_2} {β : Type u_1} {b : β} {s : (x : β) → b = xSet α} :
(Set.interᵢ fun x => Set.interᵢ fun h => s x h) = s b (_ : b = b)
@[simp]
theorem Set.unionᵢ_unionᵢ_eq_left {α : Type u_2} {β : Type u_1} {b : β} {s : (x : β) → x = bSet α} :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x h) = s b (_ : b = b)
@[simp]
theorem Set.unionᵢ_unionᵢ_eq_right {α : Type u_2} {β : Type u_1} {b : β} {s : (x : β) → b = xSet α} :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x h) = s b (_ : b = b)
theorem Set.interᵢ_or {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
(Set.interᵢ fun h => s h) = (Set.interᵢ fun h => s (_ : p q)) Set.interᵢ fun h => s (_ : p q)
theorem Set.unionᵢ_or {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
(Set.unionᵢ fun h => s h) = (Set.unionᵢ fun i => s (_ : p q)) Set.unionᵢ fun j => s (_ : p q)
theorem Set.unionᵢ_and {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
(Set.unionᵢ fun h => s h) = Set.unionᵢ fun hp => Set.unionᵢ fun hq => s (_ : p q)
theorem Set.interᵢ_and {α : Type u_1} {p : Prop} {q : Prop} (s : p qSet α) :
(Set.interᵢ fun h => s h) = Set.interᵢ fun hp => Set.interᵢ fun hq => s (_ : p q)
theorem Set.unionᵢ_comm {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} (s : ιι'Set α) :
(Set.unionᵢ fun i => Set.unionᵢ fun i' => s i i') = Set.unionᵢ fun i' => Set.unionᵢ fun i => s i i'
theorem Set.interᵢ_comm {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} (s : ιι'Set α) :
(Set.interᵢ fun i => Set.interᵢ fun i' => s i i') = Set.interᵢ fun i' => Set.interᵢ fun i => s i i'
theorem Set.unionᵢ₂_comm {α : Type u_1} {ι : Sort u_2} {κ₁ : ιSort u_3} {κ₂ : ιSort u_4} (s : (i₁ : ι) → κ₁ i₁(i₂ : ι) → κ₂ i₂Set α) :
(Set.unionᵢ fun i₁ => Set.unionᵢ fun j₁ => Set.unionᵢ fun i₂ => Set.unionᵢ fun j₂ => s i₁ j₁ i₂ j₂) = Set.unionᵢ fun i₂ => Set.unionᵢ fun j₂ => Set.unionᵢ fun i₁ => Set.unionᵢ fun j₁ => s i₁ j₁ i₂ j₂
theorem Set.interᵢ₂_comm {α : Type u_1} {ι : Sort u_2} {κ₁ : ιSort u_3} {κ₂ : ιSort u_4} (s : (i₁ : ι) → κ₁ i₁(i₂ : ι) → κ₂ i₂Set α) :
(Set.interᵢ fun i₁ => Set.interᵢ fun j₁ => Set.interᵢ fun i₂ => Set.interᵢ fun j₂ => s i₁ j₁ i₂ j₂) = Set.interᵢ fun i₂ => Set.interᵢ fun j₂ => Set.interᵢ fun i₁ => Set.interᵢ fun j₁ => s i₁ j₁ i₂ j₂
@[simp]
theorem Set.bunionᵢ_and {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} (p : ιProp) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p x q x ySet α) :
(Set.unionᵢ fun x => Set.unionᵢ fun y => Set.unionᵢ fun h => s x y h) = Set.unionᵢ fun x => Set.unionᵢ fun hx => Set.unionᵢ fun y => Set.unionᵢ fun hy => s x y (_ : p x q x y)
@[simp]
theorem Set.bunionᵢ_and' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} (p : ι'Prop) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p y q x ySet α) :
(Set.unionᵢ fun x => Set.unionᵢ fun y => Set.unionᵢ fun h => s x y h) = Set.unionᵢ fun y => Set.unionᵢ fun hy => Set.unionᵢ fun x => Set.unionᵢ fun hx => s x y (_ : p y q x y)
@[simp]
theorem Set.binterᵢ_and {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} (p : ιProp) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p x q x ySet α) :
(Set.interᵢ fun x => Set.interᵢ fun y => Set.interᵢ fun h => s x y h) = Set.interᵢ fun x => Set.interᵢ fun hx => Set.interᵢ fun y => Set.interᵢ fun hy => s x y (_ : p x q x y)
@[simp]
theorem Set.binterᵢ_and' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} (p : ι'Prop) (q : ιι'Prop) (s : (x : ι) → (y : ι') → p y q x ySet α) :
(Set.interᵢ fun x => Set.interᵢ fun y => Set.interᵢ fun h => s x y h) = Set.interᵢ fun y => Set.interᵢ fun hy => Set.interᵢ fun x => Set.interᵢ fun hx => s x y (_ : p y q x y)
@[simp]
theorem Set.unionᵢ_unionᵢ_eq_or_left {α : Type u_2} {β : Type u_1} {b : β} {p : βProp} {s : (x : β) → x = b p xSet α} :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x h) = s b (_ : b = b p b) Set.unionᵢ fun x => Set.unionᵢ fun h => s x (_ : x = b p x)
@[simp]
theorem Set.interᵢ_interᵢ_eq_or_left {α : Type u_2} {β : Type u_1} {b : β} {p : βProp} {s : (x : β) → x = b p xSet α} :
(Set.interᵢ fun x => Set.interᵢ fun h => s x h) = s b (_ : b = b p b) Set.interᵢ fun x => Set.interᵢ fun h => s x (_ : x = b p x)

### Bounded unions and intersections #

theorem Set.mem_bunionᵢ {α : Type u_1} {β : Type u_2} {s : Set α} {t : αSet β} {x : α} {y : β} (xs : x s) (ytx : y t x) :
y Set.unionᵢ fun x => Set.unionᵢ fun h => t x

A specialization of mem_unionᵢ₂.

theorem Set.mem_binterᵢ {α : Type u_1} {β : Type u_2} {s : Set α} {t : αSet β} {y : β} (h : ∀ (x : α), x sy t x) :
y Set.interᵢ fun x => Set.interᵢ fun h => t x

A specialization of mem_interᵢ₂.

theorem Set.subset_bunionᵢ_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {u : αSet β} {x : α} (xs : x s) :
u x Set.unionᵢ fun x => Set.unionᵢ fun h => u x

A specialization of subset_unionᵢ₂.

theorem Set.binterᵢ_subset_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {t : αSet β} {x : α} (xs : x s) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) t x

A specialization of interᵢ₂_subset.

theorem Set.bunionᵢ_subset_bunionᵢ_left {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} (h : s s') :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) Set.unionᵢ fun x => Set.unionᵢ fun h => t x
theorem Set.binterᵢ_subset_binterᵢ_left {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} (h : s' s) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) Set.interᵢ fun x => Set.interᵢ fun h => t x
theorem Set.bunionᵢ_mono {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} {t' : αSet β} (hs : s' s) (h : ∀ (x : α), x st x t' x) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) Set.unionᵢ fun x => Set.unionᵢ fun h => t' x
theorem Set.binterᵢ_mono {α : Type u_1} {β : Type u_2} {s : Set α} {s' : Set α} {t : αSet β} {t' : αSet β} (hs : s s') (h : ∀ (x : α), x st x t' x) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) Set.interᵢ fun x => Set.interᵢ fun h => t' x
theorem Set.bunionᵢ_eq_unionᵢ {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x sSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x h) = Set.unionᵢ fun x => t x (_ : x s)
theorem Set.binterᵢ_eq_interᵢ {α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x sSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x h) = Set.interᵢ fun x => t x (_ : x s)
theorem Set.unionᵢ_subtype {α : Type u_1} {β : Type u_2} (p : αProp) (s : { x // p x }Set β) :
(Set.unionᵢ fun x => s x) = Set.unionᵢ fun x => Set.unionᵢ fun hx => s { val := x, property := hx }
theorem Set.interᵢ_subtype {α : Type u_1} {β : Type u_2} (p : αProp) (s : { x // p x }Set β) :
(Set.interᵢ fun x => s x) = Set.interᵢ fun x => Set.interᵢ fun hx => s { val := x, property := hx }
theorem Set.binterᵢ_empty {α : Type u_2} {β : Type u_1} (u : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => u x) = Set.univ
theorem Set.binterᵢ_univ {α : Type u_2} {β : Type u_1} (u : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => u x) = Set.interᵢ fun x => u x
@[simp]
theorem Set.bunionᵢ_self {α : Type u_1} (s : Set α) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s) = s
@[simp]
theorem Set.unionᵢ_nonempty_self {α : Type u_1} (s : Set α) :
(Set.unionᵢ fun _h => s) = s
theorem Set.binterᵢ_singleton {α : Type u_2} {β : Type u_1} (a : α) (s : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => s x) = s a
theorem Set.binterᵢ_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => u x) = (Set.interᵢ fun x => Set.interᵢ fun h => u x) Set.interᵢ fun x => Set.interᵢ fun h => u x
theorem Set.binterᵢ_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) = t a Set.interᵢ fun x => Set.interᵢ fun h => t x
theorem Set.binterᵢ_pair {α : Type u_2} {β : Type u_1} (a : α) (b : α) (s : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => s x) = s a s b
theorem Set.binterᵢ_inter {ι : Type u_1} {α : Type u_2} {s : Set ι} (hs : ) (f : ιSet α) (t : Set α) :
(Set.interᵢ fun i => Set.interᵢ fun h => f i t) = (Set.interᵢ fun i => Set.interᵢ fun h => f i) t
theorem Set.inter_binterᵢ {ι : Type u_1} {α : Type u_2} {s : Set ι} (hs : ) (f : ιSet α) (t : Set α) :
(Set.interᵢ fun i => Set.interᵢ fun h => t f i) = t Set.interᵢ fun i => Set.interᵢ fun h => f i
theorem Set.bunionᵢ_empty {α : Type u_2} {β : Type u_1} (s : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x) =
theorem Set.bunionᵢ_univ {α : Type u_2} {β : Type u_1} (s : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x) = Set.unionᵢ fun x => s x
theorem Set.bunionᵢ_singleton {α : Type u_2} {β : Type u_1} (a : α) (s : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x) = s a
@[simp]
theorem Set.bunionᵢ_of_singleton {α : Type u_1} (s : Set α) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => {x}) = s
theorem Set.bunionᵢ_union {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set α) (u : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => u x) = (Set.unionᵢ fun x => Set.unionᵢ fun h => u x) Set.unionᵢ fun x => Set.unionᵢ fun h => u x
@[simp]
theorem Set.unionᵢ_coe_set {α : Type u_1} {β : Type u_2} (s : Set α) (f : sSet β) :
(Set.unionᵢ fun i => f i) = Set.unionᵢ fun i => Set.unionᵢ fun h => f { val := i, property := h }
@[simp]
theorem Set.interᵢ_coe_set {α : Type u_1} {β : Type u_2} (s : Set α) (f : sSet β) :
(Set.interᵢ fun i => f i) = Set.interᵢ fun i => Set.interᵢ fun h => f { val := i, property := h }
theorem Set.bunionᵢ_insert {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) = t a Set.unionᵢ fun x => Set.unionᵢ fun h => t x
theorem Set.bunionᵢ_pair {α : Type u_2} {β : Type u_1} (a : α) (b : α) (s : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x) = s a s b
theorem Set.inter_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : Set α) (t : (i : ι) → κ iSet α) :
(s Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s t i j
theorem Set.unionᵢ₂_inter {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : (i : ι) → κ iSet α) (t : Set α) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j t
theorem Set.union_interᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : Set α) (t : (i : ι) → κ iSet α) :
(s Set.interᵢ fun i => Set.interᵢ fun j => t i j) = Set.interᵢ fun i => Set.interᵢ fun j => s t i j
theorem Set.interᵢ₂_union {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : (i : ι) → κ iSet α) (t : Set α) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) t = Set.interᵢ fun i => Set.interᵢ fun j => s i j t
theorem Set.mem_unionₛ_of_mem {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)} (hx : x t) (ht : t S) :
theorem Set.not_mem_of_not_mem_unionₛ {α : Type u_1} {x : α} {t : Set α} {S : Set (Set α)} (hx : ¬x ⋃₀ S) (ht : t S) :
¬x t
theorem Set.interₛ_subset_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t S) :
theorem Set.subset_unionₛ_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t S) :
theorem Set.subset_unionₛ_of_subset {α : Type u_1} {s : Set α} (t : Set (Set α)) (u : Set α) (h₁ : s u) (h₂ : u t) :
theorem Set.unionₛ_subset {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : ∀ (t' : Set α), t' St' t) :
@[simp]
theorem Set.unionₛ_subset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} :
⋃₀ s t ∀ (t' : Set α), t' st' t
theorem Set.subset_interₛ {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : ∀ (t' : Set α), t' St t') :
@[simp]
theorem Set.subset_interₛ_iff {α : Type u_1} {S : Set (Set α)} {t : Set α} :
t ⋂₀ S ∀ (t' : Set α), t' St t'
theorem Set.unionₛ_subset_unionₛ {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S T) :
theorem Set.interₛ_subset_interₛ {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S T) :
@[simp]
theorem Set.unionₛ_empty {α : Type u_1} :
@[simp]
theorem Set.interₛ_empty {α : Type u_1} :
= Set.univ
@[simp]
theorem Set.unionₛ_singleton {α : Type u_1} (s : Set α) :
⋃₀ {s} = s
@[simp]
theorem Set.interₛ_singleton {α : Type u_1} (s : Set α) :
⋂₀ {s} = s
@[simp]
theorem Set.unionₛ_eq_empty {α : Type u_1} {S : Set (Set α)} :
⋃₀ S = ∀ (s : Set α), s Ss =
@[simp]
theorem Set.interₛ_eq_univ {α : Type u_1} {S : Set (Set α)} :
⋂₀ S = Set.univ ∀ (s : Set α), s Ss = Set.univ
theorem Set.unionₛ_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_unionₛ {α : Type u_1} {S : Set (Set α)} :
Set.Nonempty (⋃₀ S) s, s S
theorem Set.Nonempty.of_unionₛ {α : Type u_1} {s : Set (Set α)} (h : Set.Nonempty (⋃₀ s)) :
theorem Set.Nonempty.of_unionₛ_eq_univ {α : Type u_1} [inst : ] {s : Set (Set α)} (h : ⋃₀ s = Set.univ) :
theorem Set.unionₛ_union {α : Type u_1} (S : Set (Set α)) (T : Set (Set α)) :
theorem Set.interₛ_union {α : Type u_1} (S : Set (Set α)) (T : Set (Set α)) :
@[simp]
theorem Set.unionₛ_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) :
@[simp]
theorem Set.interₛ_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) :
@[simp]
theorem Set.unionₛ_diff_singleton_empty {α : Type u_1} (s : Set (Set α)) :
⋃₀ (s \ {}) = ⋃₀ s
@[simp]
theorem Set.interₛ_diff_singleton_univ {α : Type u_1} (s : Set (Set α)) :
⋂₀ (s \ {Set.univ}) = ⋂₀ s
theorem Set.unionₛ_pair {α : Type u_1} (s : Set α) (t : Set α) :
⋃₀ {s, t} = s t
theorem Set.interₛ_pair {α : Type u_1} (s : Set α) (t : Set α) :
⋂₀ {s, t} = s t
@[simp]
theorem Set.unionₛ_image {α : Type u_2} {β : Type u_1} (f : αSet β) (s : Set α) :
⋃₀ (f '' s) = Set.unionᵢ fun x => Set.unionᵢ fun h => f x
@[simp]
theorem Set.interₛ_image {α : Type u_2} {β : Type u_1} (f : αSet β) (s : Set α) :
⋂₀ (f '' s) = Set.interᵢ fun x => Set.interᵢ fun h => f x
@[simp]
theorem Set.unionₛ_range {β : Type u_1} {ι : Sort u_2} (f : ιSet β) :
= Set.unionᵢ fun x => f x
@[simp]
theorem Set.interₛ_range {β : Type u_1} {ι : Sort u_2} (f : ιSet β) :
= Set.interᵢ fun x => f x
theorem Set.unionᵢ_eq_univ_iff {α : Type u_1} {ι : Sort u_2} {f : ιSet α} :
(Set.unionᵢ fun i => f i) = Set.univ ∀ (x : α), i, x f i
theorem Set.unionᵢ₂_eq_univ_iff {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.univ ∀ (a : α), i j, a s i j
theorem Set.unionₛ_eq_univ_iff {α : Type u_1} {c : Set (Set α)} :
⋃₀ c = Set.univ ∀ (a : α), b, b c a b
theorem Set.interᵢ_eq_empty_iff {α : Type u_1} {ι : Sort u_2} {f : ιSet α} :
(Set.interᵢ fun i => f i) = ∀ (x : α), i, ¬x f i
theorem Set.interᵢ₂_eq_empty_iff {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) = ∀ (a : α), i j, ¬a s i j
theorem Set.interₛ_eq_empty_iff {α : Type u_1} {c : Set (Set α)} :
⋂₀ c = ∀ (a : α), b, b c ¬a b
@[simp]
theorem Set.nonempty_interᵢ {α : Type u_1} {ι : Sort u_2} {f : ιSet α} :
Set.Nonempty (Set.interᵢ fun i => f i) x, ∀ (i : ι), x f i
theorem Set.nonempty_interᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} :
Set.Nonempty (Set.interᵢ fun i => Set.interᵢ fun j => s i j) a, ∀ (i : ι) (j : κ i), a s i j
@[simp]
theorem Set.nonempty_interₛ {α : Type u_1} {c : Set (Set α)} :
Set.Nonempty (⋂₀ c) a, ∀ (b : Set α), b ca b
theorem Set.compl_unionₛ {α : Type u_1} (S : Set (Set α)) :
(⋃₀ S) = ⋂₀ (compl '' S)
theorem Set.unionₛ_eq_compl_interₛ_compl {α : Type u_1} (S : Set (Set α)) :
⋃₀ S = (⋂₀ (compl '' S))
theorem Set.compl_interₛ {α : Type u_1} (S : Set (Set α)) :
(⋂₀ S) = ⋃₀ (compl '' S)
theorem Set.interₛ_eq_compl_unionₛ_compl {α : Type u_1} (S : Set (Set α)) :
⋂₀ S = (⋃₀ (compl '' S))
theorem Set.inter_empty_of_inter_unionₛ_empty {α : Type u_1} {s : Set α} {t : Set α} {S : Set (Set α)} (hs : t S) (h : s ⋃₀ S = ) :
s t =
theorem Set.range_sigma_eq_unionᵢ_range {α : Type u_2} {β : Type u_3} {γ : αType u_1} (f : β) :
= Set.unionᵢ fun a => Set.range fun b => f { fst := a, snd := b }
theorem Set.unionᵢ_eq_range_sigma {α : Type u_2} {β : Type u_1} (s : αSet β) :
(Set.unionᵢ fun i => s i) = Set.range fun a => a.snd
theorem Set.unionᵢ_eq_range_psigma {β : Type u_1} {ι : Sort u_2} (s : ιSet β) :
(Set.unionᵢ fun i => s i) = Set.range fun a => a.snd
theorem Set.unionᵢ_image_preimage_sigma_mk_eq_self {ι : Type u_1} {σ : ιType u_2} (s : Set ()) :
(Set.unionᵢ fun i => '' ( ⁻¹' s)) = s
theorem Set.Sigma.univ {α : Type u_2} (X : αType u_1) :
Set.univ = Set.unionᵢ fun a =>
theorem Set.unionₛ_mono {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} (h : s t) :
theorem Set.unionᵢ_subset_unionᵢ_const {α : Type u_1} {ι : Sort u_2} {ι₂ : Sort u_3} {s : Set α} (h : ιι₂) :
(Set.unionᵢ fun _i => s) Set.unionᵢ fun _j => s
@[simp]
theorem Set.unionᵢ_singleton_eq_range {α : Type u_1} {β : Type u_2} (f : αβ) :
(Set.unionᵢ fun x => {f x}) =
theorem Set.unionᵢ_of_singleton (α : Type u_1) :
(Set.unionᵢ fun x => {x}) = Set.univ
theorem Set.unionᵢ_of_singleton_coe {α : Type u_1} (s : Set α) :
(Set.unionᵢ fun i => {i}) = s
theorem Set.unionₛ_eq_bunionᵢ {α : Type u_1} {s : Set (Set α)} :
⋃₀ s = Set.unionᵢ fun i => Set.unionᵢ fun _h => i
theorem Set.interₛ_eq_binterᵢ {α : Type u_1} {s : Set (Set α)} :
⋂₀ s = Set.interᵢ fun i => Set.interᵢ fun _h => i
theorem Set.unionₛ_eq_unionᵢ {α : Type u_1} {s : Set (Set α)} :
⋃₀ s = Set.unionᵢ fun i => i
theorem Set.interₛ_eq_interᵢ {α : Type u_1} {s : Set (Set α)} :
⋂₀ s = Set.interᵢ fun i => i
@[simp]
theorem Set.unionᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : ] (s : ιSet α) :
(Set.unionᵢ fun i => s i) =
@[simp]
theorem Set.interᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : ] (s : ιSet α) :
(Set.interᵢ fun i => s i) = Set.univ
theorem Set.union_eq_unionᵢ {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :
s₁ s₂ = Set.unionᵢ fun b => bif b then s₁ else s₂
theorem Set.inter_eq_interᵢ {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :
s₁ s₂ = Set.interᵢ fun b => bif b then s₁ else s₂
theorem Set.interₛ_union_interₛ {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} :
⋂₀ S ⋂₀ T = Set.interᵢ fun p => Set.interᵢ fun h => p.fst p.snd
theorem Set.unionₛ_inter_unionₛ {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} :
⋃₀ s ⋃₀ t = Set.unionᵢ fun p => Set.unionᵢ fun h => p.fst p.snd
theorem Set.bunionᵢ_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (s : ιSet α) (t : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) = Set.unionᵢ fun i => Set.unionᵢ fun x => Set.unionᵢ fun h => t x
theorem Set.binterᵢ_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (s : ιSet α) (t : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) = Set.interᵢ fun i => Set.interᵢ fun x => Set.interᵢ fun h => t x
theorem Set.unionₛ_unionᵢ {α : Type u_1} {ι : Sort u_2} (s : ιSet (Set α)) :
(⋃₀ Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => ⋃₀ s i
theorem Set.interₛ_unionᵢ {α : Type u_1} {ι : Sort u_2} (s : ιSet (Set α)) :
(⋂₀ Set.unionᵢ fun i => s i) = Set.interᵢ fun i => ⋂₀ s i
theorem Set.unionᵢ_range_eq_unionₛ {α : Type u_1} {β : Type u_2} (C : Set (Set α)) {f : (s : C) → βs} (hf : ∀ (s : C), Function.Surjective (f s)) :
(Set.unionᵢ fun y => Set.range fun s => ↑(f s y)) = ⋃₀ C
theorem Set.unionᵢ_range_eq_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (C : ιSet α) {f : (x : ι) → β↑(C x)} (hf : ∀ (x : ι), Function.Surjective (f x)) :
(Set.unionᵢ fun y => Set.range fun x => ↑(f x y)) = Set.unionᵢ fun x => C x
theorem Set.union_distrib_interᵢ_left {α : Type u_1} {ι : Sort u_2} (s : ιSet α) (t : Set α) :
(t Set.interᵢ fun i => s i) = Set.interᵢ fun i => t s i
theorem Set.union_distrib_interᵢ₂_left {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : Set α) (t : (i : ι) → κ iSet α) :
(s Set.interᵢ fun i => Set.interᵢ fun j => t i j) = Set.interᵢ fun i => Set.interᵢ fun j => s t i j
theorem Set.union_distrib_interᵢ_right {α : Type u_1} {ι : Sort u_2} (s : ιSet α) (t : Set α) :
(Set.interᵢ fun i => s i) t = Set.interᵢ fun i => s i t
theorem Set.union_distrib_interᵢ₂_right {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} (s : (i : ι) → κ iSet α) (t : Set α) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) t = Set.interᵢ fun i => Set.interᵢ fun j => s i j t

### mapsTo#

theorem Set.mapsTo_unionₛ {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {t : Set β} {f : αβ} (H : ∀ (s : Set α), s SSet.MapsTo f s t) :
theorem Set.mapsTo_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : ιSet α} {t : Set β} {f : αβ} (H : ∀ (i : ι), Set.MapsTo f (s i) t) :
Set.MapsTo f (Set.unionᵢ fun i => s i) t
theorem Set.mapsTo_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : (i : ι) → κ iSet α} {t : Set β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t) :
Set.MapsTo f (Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t
theorem Set.mapsTo_unionᵢ_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.MapsTo f (s i) (t i)) :
Set.MapsTo f (Set.unionᵢ fun i => s i) (Set.unionᵢ fun i => t i)
theorem Set.mapsTo_unionᵢ₂_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) :
Set.MapsTo f (Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) (Set.unionᵢ fun i => Set.unionᵢ fun j => t i j)
theorem Set.mapsTo_interₛ {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : αβ} (H : ∀ (t : Set β), t TSet.MapsTo f s t) :
theorem Set.mapsTo_interᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : Set α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.MapsTo f s (t i)) :
Set.MapsTo f s (Set.interᵢ fun i => t i)
theorem Set.mapsTo_interᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : Set α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)) :
Set.MapsTo f s (Set.interᵢ fun i => Set.interᵢ fun j => t i j)
theorem Set.mapsTo_interᵢ_interᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.MapsTo f (s i) (t i)) :
Set.MapsTo f (Set.interᵢ fun i => s i) (Set.interᵢ fun i => t i)
theorem Set.mapsTo_interᵢ₂_interᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) :
Set.MapsTo f (Set.interᵢ fun i => Set.interᵢ fun j => s i j) (Set.interᵢ fun i => Set.interᵢ fun j => t i j)
theorem Set.image_interᵢ_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (s : ιSet α) (f : αβ) :
(f '' Set.interᵢ fun i => s i) Set.interᵢ fun i => f '' s i
theorem Set.image_interᵢ₂_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} (s : (i : ι) → κ iSet α) (f : αβ) :
(f '' Set.interᵢ fun i => Set.interᵢ fun j => s i j) Set.interᵢ fun i => Set.interᵢ fun j => f '' s i j
theorem Set.image_interₛ_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (f : αβ) :
f '' ⋂₀ S Set.interᵢ fun s => Set.interᵢ fun h => f '' s

### restrictPreimage#

theorem Set.injective_iff_injective_of_unionᵢ_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : αβ} {U : ιSet β} (hU : = Set.univ) :
theorem Set.surjective_iff_surjective_of_unionᵢ_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : αβ} {U : ιSet β} (hU : = Set.univ) :
theorem Set.bijective_iff_bijective_of_unionᵢ_eq_univ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : αβ} {U : ιSet β} (hU : = Set.univ) :

### InjOn#

theorem Set.InjOn.image_interᵢ_eq {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : ] {s : ιSet α} {f : αβ} (h : Set.InjOn f (Set.unionᵢ fun i => s i)) :
(f '' Set.interᵢ fun i => s i) = Set.interᵢ fun i => f '' s i
theorem Set.InjOn.image_binterᵢ_eq {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {p : ιProp} {s : (i : ι) → p iSet α} (hp : i, p i) {f : αβ} (h : Set.InjOn f (Set.unionᵢ fun i => Set.unionᵢ fun hi => s i hi)) :
(f '' Set.interᵢ fun i => Set.interᵢ fun hi => s i hi) = Set.interᵢ fun i => Set.interᵢ fun hi => f '' s i hi
theorem Set.image_interᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : αβ} (hf : ) (s : ιSet α) :
(f '' Set.interᵢ fun i => s i) = Set.interᵢ fun i => f '' s i
theorem Set.image_interᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {f : αβ} (hf : ) (s : (i : ι) → κ iSet α) :
(f '' Set.interᵢ fun i => Set.interᵢ fun j => s i j) = Set.interᵢ fun i => Set.interᵢ fun j => f '' s i j
theorem Set.inj_on_unionᵢ_of_directed {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {s : ιSet α} (hs : Directed (fun x x_1 => x x_1) s) {f : αβ} (hf : ∀ (i : ι), Set.InjOn f (s i)) :
Set.InjOn f (Set.unionᵢ fun i => s i)

### SurjOn#

theorem Set.surjOn_unionₛ {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : αβ} (H : ∀ (t : Set β), t TSet.SurjOn f s t) :
theorem Set.surjOn_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : Set α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f s (t i)) :
Set.SurjOn f s (Set.unionᵢ fun i => t i)
theorem Set.surjOn_unionᵢ_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f (s i) (t i)) :
Set.SurjOn f (Set.unionᵢ fun i => s i) (Set.unionᵢ fun i => t i)
theorem Set.surjOn_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : Set α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.SurjOn f s (t i j)) :
Set.SurjOn f s (Set.unionᵢ fun i => Set.unionᵢ fun j => t i j)
theorem Set.surjOn_unionᵢ₂_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : (i : ι) → κ iSet α} {t : (i : ι) → κ iSet β} {f : αβ} (H : ∀ (i : ι) (j : κ i), Set.SurjOn f (s i j) (t i j)) :
Set.SurjOn f (Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) (Set.unionᵢ fun i => Set.unionᵢ fun j => t i j)
theorem Set.surjOn_interᵢ {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : ] {s : ιSet α} {t : Set β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f (s i) t) (Hinj : Set.InjOn f (Set.unionᵢ fun i => s i)) :
Set.SurjOn f (Set.interᵢ fun i => s i) t
theorem Set.surjOn_interᵢ_interᵢ {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : ] {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.SurjOn f (s i) (t i)) (Hinj : Set.InjOn f (Set.unionᵢ fun i => s i)) :
Set.SurjOn f (Set.interᵢ fun i => s i) (Set.interᵢ fun i => t i)

### BijOn#

theorem Set.bijOn_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.BijOn f (s i) (t i)) (Hinj : Set.InjOn f (Set.unionᵢ fun i => s i)) :
Set.BijOn f (Set.unionᵢ fun i => s i) (Set.unionᵢ fun i => t i)
theorem Set.bijOn_interᵢ {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [hi : ] {s : ιSet α} {t : ιSet β} {f : αβ} (H : ∀ (i : ι), Set.BijOn f (s i) (t i)) (Hinj : Set.InjOn f (Set.unionᵢ fun i => s i)) :
Set.BijOn f (Set.interᵢ fun i => s i) (Set.interᵢ fun i => t i)
theorem Set.bijOn_unionᵢ_of_directed {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {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 (Set.unionᵢ fun i => s i) (Set.unionᵢ fun i => t i)
theorem Set.bijOn_interᵢ_of_directed {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : ] {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 (Set.interᵢ fun i => s i) (Set.interᵢ fun i => t i)

### image, preimage#

theorem Set.image_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {f : αβ} {s : ιSet α} :
(f '' Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => f '' s i
theorem Set.image_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} (f : αβ) (s : (i : ι) → κ iSet α) :
(f '' Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => f '' s i j
theorem Set.univ_subtype {α : Type u_1} {p : αProp} :
Set.univ = Set.unionᵢ fun x => Set.unionᵢ fun h => {{ val := x, property := h }}
theorem Set.range_eq_unionᵢ {α : Type u_2} {ι : Sort u_1} (f : ια) :
= Set.unionᵢ fun i => {f i}
theorem Set.image_eq_unionᵢ {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
f '' s = Set.unionᵢ fun i => Set.unionᵢ fun h => {f i}
theorem Set.bunionᵢ_range {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {f : ια} {g : αSet β} :
(Set.unionᵢ fun x => Set.unionᵢ fun h => g x) = Set.unionᵢ fun y => g (f y)
@[simp]
theorem Set.unionᵢ_unionᵢ_eq' {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {f : ια} {g : αSet β} :
(Set.unionᵢ fun x => Set.unionᵢ fun y => Set.unionᵢ fun _h => g x) = Set.unionᵢ fun y => g (f y)
theorem Set.binterᵢ_range {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {f : ια} {g : αSet β} :
(Set.interᵢ fun x => Set.interᵢ fun h => g x) = Set.interᵢ fun y => g (f y)
@[simp]
theorem Set.interᵢ_interᵢ_eq' {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {f : ια} {g : αSet β} :
(Set.interᵢ fun x => Set.interᵢ fun y => Set.interᵢ fun _h => g x) = Set.interᵢ fun y => g (f y)
theorem Set.bunionᵢ_image {α : Type u_2} {β : Type u_1} {γ : Type u_3} {s : Set γ} {f : γα} {g : αSet β} :
(Set.unionᵢ fun x => Set.unionᵢ fun h => g x) = Set.unionᵢ fun y => Set.unionᵢ fun h => g (f y)
theorem Set.binterᵢ_image {α : Type u_2} {β : Type u_1} {γ : Type u_3} {s : Set γ} {f : γα} {g : αSet β} :
(Set.interᵢ fun x => Set.interᵢ fun h => g x) = Set.interᵢ fun y => Set.interᵢ fun h => g (f y)
theorem Set.monotone_preimage {α : Type u_2} {β : Type u_1} {f : αβ} :
@[simp]
theorem Set.preimage_unionᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {f : αβ} {s : ιSet β} :
(f ⁻¹' Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => f ⁻¹' s i
theorem Set.preimage_unionᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} {f : αβ} {s : (i : ι) → κ iSet β} :
(f ⁻¹' Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => f ⁻¹' s i j
@[simp]
theorem Set.preimage_unionₛ {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set (Set β)} :
f ⁻¹' ⋃₀ s = Set.unionᵢ fun t => Set.unionᵢ fun h => f ⁻¹' t
theorem Set.preimage_interᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {f : αβ} {s : ιSet β} :
(f ⁻¹' Set.interᵢ fun i => s i) = Set.interᵢ fun i => f ⁻¹' s i
theorem Set.preimage_interᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} {f : αβ} {s : (i : ι) → κ iSet β} :
(f ⁻¹' Set.interᵢ fun i => Set.interᵢ fun j => s i j) = Set.interᵢ fun i => Set.interᵢ fun j => f ⁻¹' s i j
@[simp]
theorem Set.preimage_interₛ {α : Type u_2} {β : Type u_1} {f : αβ} {s : Set (Set β)} :
f ⁻¹' ⋂₀ s = Set.interᵢ fun t => Set.interᵢ fun h => f ⁻¹' t
@[simp]
theorem Set.bunionᵢ_preimage_singleton {α : Type u_2} {β : Type u_1} (f : αβ) (s : Set β) :
(Set.unionᵢ fun y => Set.unionᵢ fun h => f ⁻¹' {y}) = f ⁻¹' s
theorem Set.bunionᵢ_range_preimage_singleton {α : Type u_1} {β : Type u_2} (f : αβ) :
(Set.unionᵢ fun y => Set.unionᵢ fun h => f ⁻¹' {y}) = Set.univ
theorem Set.prod_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : Set α} {t : ιSet β} :
(s ×ˢ Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s ×ˢ t i
theorem Set.prod_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : Set α} {t : (i : ι) → κ iSet β} :
(s ×ˢ Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s ×ˢ t i j
theorem Set.prod_unionₛ {α : Type u_1} {β : Type u_2} {s : Set α} {C : Set (Set β)} :
s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)
theorem Set.unionᵢ_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {s : ιSet α} {t : Set β} :
(Set.unionᵢ fun i => s i) ×ˢ t = Set.unionᵢ fun i => s i ×ˢ t
theorem Set.unionᵢ₂_prod_const {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} {s : (i : ι) → κ iSet α} {t : Set β} :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) ×ˢ t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j ×ˢ t
theorem Set.unionₛ_prod_const {α : Type u_1} {β : Type u_2} {C : Set (Set α)} {t : Set β} :
⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)
theorem Set.unionᵢ_prod {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} (s : ιSet α) (t : ι'Set β) :
(Set.unionᵢ fun x => s x.fst ×ˢ t x.snd) = (Set.unionᵢ fun i => s i) ×ˢ Set.unionᵢ fun i => t i
theorem Set.unionᵢ_prod_of_monotone {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ] {s : αSet β} {t : αSet γ} (hs : ) (ht : ) :
(Set.unionᵢ fun x => s x ×ˢ t x) = (Set.unionᵢ fun x => s x) ×ˢ Set.unionᵢ fun x => t x
theorem Set.interₛ_prod_interₛ_subset {α : Type u_1} {β : Type u_2} (S : Set (Set α)) (T : Set (Set β)) :
⋂₀ S ×ˢ ⋂₀ T Set.interᵢ fun r => Set.interᵢ fun h => r.fst ×ˢ r.snd
theorem Set.interₛ_prod_interₛ {α : Type u_1} {β : Type u_2} {S : Set (Set α)} {T : Set (Set β)} (hS : ) (hT : ) :
⋂₀ S ×ˢ ⋂₀ T = Set.interᵢ fun r => Set.interᵢ fun h => r.fst ×ˢ r.snd
theorem Set.interₛ_prod {α : Type u_1} {β : Type u_2} {S : Set (Set α)} (hS : ) (t : Set β) :
⋂₀ S ×ˢ t = Set.interᵢ fun s => Set.interᵢ fun h => s ×ˢ t
theorem Set.prod_interₛ {α : Type u_2} {β : Type u_1} {T : Set (Set β)} (hT : ) (s : Set α) :
s ×ˢ ⋂₀ T = Set.interᵢ fun t => Set.interᵢ fun h => s ×ˢ t
theorem Set.unionᵢ_image_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} (f : αβγ) {s : Set α} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => f a '' t) = Set.image2 f s t
theorem Set.unionᵢ_image_right {α : Type u_3} {β : Type u_2} {γ : Type u_1} (f : αβγ) {s : Set α} {t : Set β} :
(Set.unionᵢ fun b => Set.unionᵢ fun h => (fun a => f a b) '' s) = Set.image2 f s t
theorem Set.image2_unionᵢ_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : ιSet α) (t : Set β) :
Set.image2 f (Set.unionᵢ fun i => s i) t = Set.unionᵢ fun i => Set.image2 f (s i) t
theorem Set.image2_unionᵢ_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : Set α) (t : ιSet β) :
Set.image2 f s (Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => Set.image2 f s (t i)
theorem Set.image2_unionᵢ₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_5} (f : αβγ) (s : (i : ι) → κ iSet α) (t : Set β) :
Set.image2 f (Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t = Set.unionᵢ fun i => Set.unionᵢ fun j => Set.image2 f (s i j) t
theorem Set.image2_unionᵢ₂_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_5} (f : αβγ) (s : Set α) (t : (i : ι) → κ iSet β) :
Set.image2 f s (Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => Set.image2 f s (t i j)
theorem Set.image2_interᵢ_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : ιSet α) (t : Set β) :
Set.image2 f (Set.interᵢ fun i => s i) t Set.interᵢ fun i => Set.image2 f (s i) t
theorem Set.image2_interᵢ_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : αβγ) (s : Set α) (t : ιSet β) :
Set.image2 f s (Set.interᵢ fun i => t i) Set.interᵢ fun i => Set.image2 f s (t i)
theorem Set.image2_interᵢ₂_subset_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_5} (f : αβγ) (s : (i : ι) → κ iSet α) (t : Set β) :
Set.image2 f (Set.interᵢ fun i => Set.interᵢ fun j => s i j) t Set.interᵢ fun i => Set.interᵢ fun j => Set.image2 f (s i j) t
theorem Set.image2_interᵢ₂_subset_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ιSort u_5} (f : αβγ) (s : Set α) (t : (i : ι) → κ iSet β) :
Set.image2 f s (Set.interᵢ fun i => Set.interᵢ fun j => t i j) Set.interᵢ fun i => Set.interᵢ fun j => Set.image2 f s (t i j)
theorem Set.image2_eq_unionᵢ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (s : Set α) (t : Set β) :
Set.image2 f s t = Set.unionᵢ fun i => Set.unionᵢ fun h => Set.unionᵢ fun j => Set.unionᵢ fun h => {f i j}

The Set.image2 version of Set.image_eq_unionᵢ

theorem Set.prod_eq_bunionᵢ_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
s ×ˢ t = Set.unionᵢ fun a => Set.unionᵢ fun h => (fun b => (a, b)) '' t
theorem Set.prod_eq_bunionᵢ_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
s ×ˢ t = Set.unionᵢ fun b => Set.unionᵢ fun h => (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∈ s.

Equations
theorem Set.seq_def {α : Type u_1} {β : Type u_2} {s : Set (αβ)} {t : Set α} :
Set.seq s t = Set.unionᵢ fun f => Set.unionᵢ fun h => 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 tf 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_3} {β : Type u_1} {γ : Type u_2} {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_2} (i : Set α) (s : (a : α) → Set (π a)) :
Set.pi i s = Set.interᵢ fun a => Set.interᵢ fun h => ⁻¹' s a
theorem Set.univ_pi_eq_interᵢ {α : Type u_2} {π : αType u_1} (t : (i : α) → Set (π i)) :
Set.pi Set.univ t = Set.interᵢ fun i => ⁻¹' t i
theorem Set.pi_diff_pi_subset {α : Type u_1} {π : αType u_2} (i : Set α) (s : (a : α) → Set (π a)) (t : (a : α) → Set (π a)) :
Set.pi i s \ Set.pi i t Set.unionᵢ fun a => Set.unionᵢ fun h => ⁻¹' (s a \ t a)
theorem Set.unionᵢ_univ_pi {α : Type u_2} {ι : Sort u_3} {π : αType u_1} (t : (i : α) → ιSet (π i)) :
(Set.unionᵢ fun x => Set.pi Set.univ fun i => t i (x i)) = Set.pi Set.univ fun i => Set.unionᵢ fun j => t i j
theorem Function.Surjective.unionᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι₂ : Sort u_2} {f : ιι₂} (hf : ) (g : ι₂Set α) :
(Set.unionᵢ fun x => g (f x)) = Set.unionᵢ fun y => g y
theorem Function.Surjective.interᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι₂ : Sort u_2} {f : ιι₂} (hf : ) (g : ι₂Set α) :
(Set.interᵢ fun x => g (f x)) = Set.interᵢ fun y => g y

### Disjoint sets #

@[simp]
theorem Set.disjoint_unionᵢ_left {α : Type u_2} {t : Set α} {ι : Sort u_1} {s : ιSet α} :
Disjoint (Set.unionᵢ fun i => s i) t ∀ (i : ι), Disjoint (s i) t
@[simp]
theorem Set.disjoint_unionᵢ_right {α : Type u_2} {t : Set α} {ι : Sort u_1} {s : ιSet α} :
Disjoint t (Set.unionᵢ fun i => s i) ∀ (i : ι), Disjoint t (s i)
theorem Set.disjoint_unionᵢ₂_left {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : (i : ι) → κ iSet α} {t : Set α} :
Disjoint (Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t ∀ (i : ι) (j : κ i), Disjoint (s i j) t
theorem Set.disjoint_unionᵢ₂_right {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {s : Set α} {t : (i : ι) → κ iSet α} :
Disjoint s (Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) ∀ (i : ι) (j : κ i), Disjoint s (t i j)
@[simp]
theorem Set.disjoint_unionₛ_left {α : Type u_1} {S : Set (Set α)} {t : Set α} :
Disjoint (⋃₀ S) t ∀ (s : Set α), s SDisjoint s t
@[simp]
theorem Set.disjoint_unionₛ_right {α : Type u_1} {s : Set α} {S : Set (Set α)} :
Disjoint s (⋃₀ S) ∀ (t : Set α), t SDisjoint s t

### Intervals #

theorem Set.Ici_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : ] (f : ια) :
Set.Ici (i, f i) = Set.interᵢ fun i => Set.Ici (f i)
theorem Set.Iic_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : ] (f : ια) :
Set.Iic (i, f i) = Set.interᵢ fun i => Set.Iic (f i)
theorem Set.Ici_supᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : ] (f : (i : ι) → κ iα) :
Set.Ici (i, j, f i j) = Set.interᵢ fun i => Set.interᵢ fun j => Set.Ici (f i j)
theorem Set.Iic_infᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : ] (f : (i : ι) → κ iα) :
Set.Iic (i, j, f i j) = Set.interᵢ fun i => Set.interᵢ fun j => Set.Iic (f i j)
theorem Set.Ici_supₛ {α : Type u_1} [inst : ] (s : Set α) :
Set.Ici (supₛ s) = Set.interᵢ fun a => Set.interᵢ fun h =>
theorem Set.Iic_infₛ {α : Type u_1} [inst : ] (s : Set α) :
Set.Iic (infₛ s) = Set.interᵢ fun a => Set.interᵢ fun h =>
theorem Set.bunionᵢ_diff_bunionᵢ_subset {α : Type u_1} {β : Type u_2} (t : αSet β) (s₁ : Set α) (s₂ : Set α) :
((Set.unionᵢ fun x => Set.unionᵢ fun h => t x) \ Set.unionᵢ fun x => Set.unionᵢ fun h => t x) Set.unionᵢ fun x => Set.unionᵢ fun h => t x
def Set.sigmaToUnionᵢ {α : Type u_1} {β : Type u_2} (t : αSet β) (x : (i : α) × ↑(t i)) :
↑(Set.unionᵢ fun 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⋃ i, t i sending ⟨i, x⟩ to x`.

Equations
• = { val := x.snd, property := (_ : x.snd Set.unionᵢ fun i => t i) }
theorem Set.sigmaToUnionᵢ_surjective {α : Type u_1} {β : Type u_2} (t : αSet β) :
theorem Set.sigmaToUnionᵢ_injective {α : Type u_1} {β : Type u_2} (t : αSet β) (h : ∀ (i j : α), i jDisjoint (t i) (t j)) :
theorem Set.sigmaToUnionᵢ_bijective {α : Type u_1} {β : Type u_2} (t : αSet β) (h : ∀ (i j : α), i jDisjoint (t i) (t j)) :
noncomputable def Set.unionEqSigmaOfDisjoint {α : Type u_1} {β : Type u_2} {t : αSet β} (h : ∀ (i j : α), i jDisjoint (t i) (t j)) :
↑(Set.unionᵢ fun i => t i) (i : α) × ↑(t i)

Equivalence between a disjoint union and a dependent sum.

Equations
theorem Set.unionᵢ_ge_eq_unionᵢ_nat_add {α : Type u_1} (u : Set α) (n : ) :
(Set.unionᵢ fun i => Set.unionᵢ fun h => u i) = Set.unionᵢ fun i => u (i + n)
theorem Set.interᵢ_ge_eq_interᵢ_nat_add {α : Type u_1} (u : Set α) (n : ) :
(Set.interᵢ fun i => Set.interᵢ fun h => u i) = Set.interᵢ fun i => u (i + n)
theorem Monotone.unionᵢ_nat_add {α : Type u_1} {f : Set α} (hf : ) (k : ) :
(Set.unionᵢ fun n => f (n + k)) = Set.unionᵢ fun n => f n
theorem Antitone.interᵢ_nat_add {α : Type u_1} {f : Set α} (hf : ) (k : ) :
(Set.interᵢ fun n => f (n + k)) = Set.interᵢ fun n => f n
theorem Set.unionᵢ_interᵢ_ge_nat_add {α : Type u_1} (f : Set α) (k : ) :
(Set.unionᵢ fun n => Set.interᵢ fun i => Set.interᵢ fun h => f (i + k)) = Set.unionᵢ fun n => Set.interᵢ fun i => Set.interᵢ fun h => f i
theorem Set.union_unionᵢ_nat_succ {α : Type u_1} (u : Set α) :
(u 0 Set.unionᵢ fun i => u (i + 1)) = Set.unionᵢ fun i => u i
theorem Set.inter_interᵢ_nat_succ {α : Type u_1} (u : Set α) :
(u 0 Set.interᵢ fun i => u (i + 1)) = Set.interᵢ fun i => u i
theorem supᵢ_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : ] (s : ιSet α) (f : αβ) :
(a, h, f a) = i, a, h, f a
theorem infᵢ_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : ] (s : ιSet α) (f : αβ) :
(a, h, f a) = i, a, h, f a
theorem supₛ_unionₛ {β : Type u_1} [inst : ] (s : Set (Set β)) :
supₛ (⋃₀ s) = t, h, supₛ t
theorem infₛ_unionₛ {β : Type u_1} [inst : ] (s : Set (Set β)) :
infₛ (⋃₀ s) = t, h, infₛ t