Documentation

instance Set.instInfSetSet {α : Type u_1} :

InfSet (Set α)

Equations

Set.instInfSetSet = { infₛ := fun s => { a | ∀ (t : Set α), t ∈ s → a ∈ 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

⋂₀ S = infₛ S

def Set.«term⋂₀_» :

Notation for Set.interₛ 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))

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

Set α

Intersection of a set of sets.

Equations

⋃₀ S = supₛ S

def Set.«term⋃₀_» :

Notation for Set.unionₛ`. 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))

@[simp]

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

x ∈ ⋂₀ S ↔ ∀ (t : Set α), t ∈ S → x ∈ 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

Set.unionᵢ s = supᵢ s

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

Set β

Indexed intersection of a family of sets

Equations

Set.interᵢ s = infᵢ s

def Set.«⋃_,_» :

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

Equations

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

def Set.«⋂_,_» :

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

supₛ S = ⋃₀ S

@[simp]

theorem Set.infₛ_eq_interₛ {α : Type u_1} (S : Set (Set α)) :

infₛ S = ⋂₀ S

@[simp]

theorem Set.supᵢ_eq_unionᵢ {α : Type u_1} {ι : Sort u_2} (s : ι → Set α) :

supᵢ s = Set.unionᵢ s

@[simp]

theorem Set.infᵢ_eq_interᵢ {α : Type u_1} {ι : Sort u_2} (s : ι → Set α) :

infᵢ s = Set.interᵢ s

@[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 : ι) → κ i → Set γ} :

(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 : ι) → κ i → Set γ} :

(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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} {a : α} (h : ∀ (i : ι) (j : κ i), a ∈ s i j) :

a ∈ Set.interᵢ fun i => Set.interᵢ fun j => s i j

instance Set.instCompleteBooleanAlgebraSet {α : Type u_1} :

CompleteBooleanAlgebra (Set α)

Equations

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

theorem Set.image_preimage {α : Type u_1} {β : Type u_2} {f : α → β} :

GaloisConnection (Set.image f) (Set.preimage f)

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

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

theorem Set.preimage_kernImage {α : Type u_2} {β : Type u_1} {f : α → β} :

GaloisConnection (Set.preimage f) (Set.kernImage f)

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.unionᵢ_congr_Prop {α : Type u_1} {p : Prop} {q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) :

Set.unionᵢ f₁ = Set.unionᵢ f₂

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

Set.interᵢ f₁ = Set.interᵢ f₂

theorem Set.unionᵢ_plift_up {α : Type u_2} {ι : Sort u_1} (f : PLift ι → 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 : PLift ι → 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 : Decidable p] (s : Set α) :

(Set.unionᵢ fun _h => s) = if p then s else ∅

theorem Set.unionᵢ_eq_dif {α : Type u_1} {p : Prop} [inst : Decidable p] (s : p → Set α) :

(Set.unionᵢ fun h => s h) = if h : p then s h else ∅

theorem Set.interᵢ_eq_if {α : Type u_1} {p : Prop} [inst : Decidable p] (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 : Decidable p] (s : p → Set α) :

(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 : Nonempty α) (w : (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) = ⊤) :

Set.Nonempty t

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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} :

(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 : ι) → κ i → Set α} (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 : ι) → κ i → Set α} (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 : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} {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 : Function.Surjective h) (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 : Function.Surjective h) (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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set α} (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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set α} (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 : Nonempty ι] (s : Set β) :

(Set.unionᵢ fun _i => s) = s

theorem Set.interᵢ_const {β : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] (s : Set β) :

(Set.interᵢ fun _i => s) = s

theorem Set.unionᵢ_eq_const {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] {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 : Nonempty ι] {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 : ι) → κ i → Set α) :

(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 : ι) → κ i → Set α) :

(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 : Nonempty ι] (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 : Nonempty ι] (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 : Nonempty ι] (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 : Nonempty ι] (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 : Nonempty ι] (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 : Preorder ι] [inst : IsDirected ι fun x x_1 => x ≤ x_1] {s : ι → Set α} {t : ι → Set α} (hs : Monotone s) (ht : Monotone t) :

(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 : Preorder ι] [inst : IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)] {s : ι → Set α} {t : ι → Set α} (hs : Antitone s) (ht : Antitone t) :

(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 : Preorder ι] [inst : IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)] {s : ι → Set α} {t : ι → Set α} (hs : Monotone s) (ht : Monotone t) :

(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 : Preorder ι] [inst : IsDirected ι fun x x_1 => x ≤ x_1] {s : ι → Set α} {t : ι → Set α} (hs : Antitone s) (ht : Antitone t) :

(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 : Option ι → 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 : Option ι → 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 : DecidablePred p] (f : (i : ι) → p i → Set α) (g : (i : ι) → ¬p i → Set α) :

(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 : DecidablePred p] (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 : DecidablePred p] (f : (i : ι) → p i → Set α) (g : (i : ι) → ¬p i → Set α) :

(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 : DecidablePred p] (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 : False → Set α} :

Set.interᵢ s = Set.univ

theorem Set.unionᵢ_false {α : Type u_1} {s : False → Set α} :

Set.unionᵢ s = ∅

@[simp]

theorem Set.interᵢ_true {α : Type u_1} {s : True → Set α} :

Set.interᵢ s = s trivial

@[simp]

theorem Set.unionᵢ_true {α : Type u_1} {s : True → Set α} :

Set.unionᵢ s = s trivial

@[simp]

theorem Set.interᵢ_exists {α : Type u_2} {ι : Sort u_1} {p : ι → Prop} {f : Exists p → Set α} :

(Set.interᵢ fun x => f x) = Set.interᵢ fun i => Set.interᵢ fun h => f (_ : Exists p)

@[simp]

theorem Set.unionᵢ_exists {α : Type u_2} {ι : Sort u_1} {p : ι → Prop} {f : Exists p → Set α} :

(Set.unionᵢ fun x => f x) = Set.unionᵢ fun i => Set.unionᵢ fun h => f (_ : Exists p)

@[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.Nonempty s → 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 = b → Set α} :

(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 = x → Set α} :

(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 = b → Set α} :

(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 = x → Set α} :

(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 ∨ q → Set α) :

(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 ∨ q → Set α) :

(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 ∧ q → Set α) :

(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 ∧ q → Set α) :

(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 y → Set α) :

(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 y → Set α) :

(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 y → Set α) :

(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 y → Set α) :

(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 x → Set α} :

(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 x → Set α} :

(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 ∈ s → y ∈ 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 ∈ s → t 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 ∈ s → t 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 ∈ s → Set β) :

(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 ∈ s → Set β) :

(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 : Set.Nonempty s) (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 : Set.Nonempty s) (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 : ↑s → Set β) :

(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 : ↑s → Set β) :

(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 : ι) → κ i → Set α) :

(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 : ι) → κ i → Set α) (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 : ι) → κ i → Set α) :

(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 : ι) → κ i → Set α) (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) :

x ∈ ⋃₀ 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) :

⋂₀ S ⊆ t

theorem Set.subset_unionₛ_of_mem {α : Type u_1} {S : Set (Set α)} {t : Set α} (tS : t ∈ S) :

t ⊆ ⋃₀ S

theorem Set.subset_unionₛ_of_subset {α : Type u_1} {s : Set α} (t : Set (Set α)) (u : Set α) (h₁ : s ⊆ u) (h₂ : u ∈ t) :

s ⊆ ⋃₀ t

theorem Set.unionₛ_subset {α : Type u_1} {S : Set (Set α)} {t : Set α} (h : ∀ (t' : Set α), t' ∈ S → t' ⊆ t) :

⋃₀ S ⊆ t

@[simp]

theorem Set.unionₛ_subset_iff {α : Type u_1} {s : Set (Set α)} {t : Set α} :

⋃₀ s ⊆ t ↔ ∀ (t' : Set α), t' ∈ s → t' ⊆ t

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

t ⊆ ⋂₀ S

@[simp]

theorem Set.subset_interₛ_iff {α : Type u_1} {S : Set (Set α)} {t : Set α} :

t ⊆ ⋂₀ S ↔ ∀ (t' : Set α), t' ∈ S → t ⊆ t'

theorem Set.unionₛ_subset_unionₛ {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S ⊆ T) :

⋃₀ S ⊆ ⋃₀ T

theorem Set.interₛ_subset_interₛ {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (h : S ⊆ T) :

⋂₀ T ⊆ ⋂₀ S

@[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 ∈ S → s = ∅

@[simp]

theorem Set.interₛ_eq_univ {α : Type u_1} {S : Set (Set α)} :

⋂₀ S = Set.univ ↔ ∀ (s : Set α), s ∈ S → s = 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 ∧ Set.Nonempty s

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

Set.Nonempty s

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

Set.Nonempty s

theorem Set.unionₛ_union {α : Type u_1} (S : Set (Set α)) (T : Set (Set α)) :

⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T

theorem Set.interₛ_union {α : Type u_1} (S : Set (Set α)) (T : Set (Set α)) :

⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T

@[simp]

theorem Set.unionₛ_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) :

⋃₀ insert s T = s ∪ ⋃₀ T

@[simp]

theorem Set.interₛ_insert {α : Type u_1} (s : Set α) (T : Set (Set α)) :

⋂₀ insert s T = s ∩ ⋂₀ T

@[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.range f = Set.unionᵢ fun x => f x

@[simp]

theorem Set.interₛ_range {β : Type u_1} {ι : Sort u_2} (f : ι → Set β) :

⋂₀ Set.range f = 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 : ι) → κ i → Set α} :

(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 : ι) → κ i → Set α} :

(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 : ι) → κ i → Set α} :

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 ∈ c → a ∈ 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 : Sigma γ → β) :

Set.range 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 (Sigma σ)) :

(Set.unionᵢ fun i => Sigma.mk i '' (Sigma.mk i ⁻¹' s)) = s

theorem Set.Sigma.univ {α : Type u_2} (X : α → Type u_1) :

Set.univ = Set.unionᵢ fun a => Set.range (Sigma.mk a)

theorem Set.unionₛ_mono {α : Type u_1} {s : Set (Set α)} {t : Set (Set α)} (h : s ⊆ t) :

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

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 : IsEmpty ι] (s : ι → Set α) :

(Set.unionᵢ fun i => s i) = ∅

@[simp]

theorem Set.interᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : IsEmpty ι] (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 : ι) → κ i → Set α) :

(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 : ι) → κ i → Set α) (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 ∈ S → Set.MapsTo f s t) :

Set.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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {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 ∈ T → Set.MapsTo f s t) :

Set.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 : ι) → κ i → Set β} {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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {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 : ι) → κ i → Set α) (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.unionᵢ U = Set.univ) :

Function.Injective f ↔ ∀ (i : ι), Function.Injective (Set.restrictPreimage (U i) f)

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

Function.Surjective f ↔ ∀ (i : ι), Function.Surjective (Set.restrictPreimage (U i) f)

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

Function.Bijective f ↔ ∀ (i : ι), Function.Bijective (Set.restrictPreimage (U i) f)

`InjOn` #

theorem Set.InjOn.image_interᵢ_eq {α : Type u_2} {β : Type u_3} {ι : Sort u_1} [inst : Nonempty ι] {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 i → Set α} (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 : Function.Bijective f) (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 : Function.Bijective f) (s : (i : ι) → κ i → Set α) :

(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 ∈ T → Set.SurjOn f s t) :

Set.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 : ι) → κ i → Set β} {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 : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {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 : Nonempty ι] {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 : Nonempty ι] {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 : Nonempty ι] {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 : 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 (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 : ι) → κ i → Set α) :

(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.range 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 : α → β} :

Monotone (Set.preimage 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 : ι) → κ i → Set β} :

(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 : ι) → κ i → Set β} :

(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 : ι) → κ i → Set β} :

(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 : ι) → κ i → Set α} {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 : SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) :

(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 : Set.Nonempty S) (hT : Set.Nonempty T) :

⋂₀ 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 : Set.Nonempty S) (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 : Set.Nonempty T) (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 : ι) → κ i → Set α) (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 : ι) → κ i → Set β) :

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 : ι) → κ i → Set α) (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 : ι) → κ i → Set β) :

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

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

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 ∈ 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_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 => Function.eval a ⁻¹' 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 => Function.eval 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 => Function.eval a ⁻¹' (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 : Function.Surjective f) (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 : Function.Surjective f) (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 : ι) → κ i → Set α} {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 : ι) → κ i → Set α} :

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 ∈ S → Disjoint s t

@[simp]

theorem Set.disjoint_unionₛ_right {α : Type u_1} {s : Set α} {S : Set (Set α)} :

Disjoint s (⋃₀ S) ↔ ∀ (t : Set α), t ∈ S → Disjoint s t

Intervals #

theorem Set.Ici_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (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 : CompleteLattice α] (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 : CompleteLattice α] (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 : CompleteLattice α] (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 : CompleteLattice α] (s : Set α) :

Set.Ici (supₛ s) = Set.interᵢ fun a => Set.interᵢ fun h => Set.Ici a

theorem Set.Iic_infₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set α) :

Set.Iic (infₛ s) = Set.interᵢ fun a => Set.interᵢ fun h => Set.Iic a

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

Set.sigmaToUnionᵢ t x = { val := ↑x.snd, property := (_ : ↑x.snd ∈ Set.unionᵢ fun i => t i) }

theorem Set.sigmaToUnionᵢ_surjective {α : Type u_1} {β : Type u_2} (t : α → Set β) :

Function.Surjective (Set.sigmaToUnionᵢ t)

theorem Set.sigmaToUnionᵢ_injective {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)) :

Function.Injective (Set.sigmaToUnionᵢ t)

theorem Set.sigmaToUnionᵢ_bijective {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)) :

Function.Bijective (Set.sigmaToUnionᵢ t)

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

↑(Set.unionᵢ fun i => t i) ≃ (i : α) × ↑(t i)

Equivalence between a disjoint union and a dependent sum.

Equations

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

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 : Monotone f) (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 : Antitone f) (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 : CompleteLattice β] (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 : CompleteLattice β] (s : ι → Set α) (f : α → β) :

(⨅ a, ⨅ h, f a) = ⨅ i, ⨅ a, ⨅ h, f a

theorem supₛ_unionₛ {β : Type u_1} [inst : CompleteLattice β] (s : Set (Set β)) :

supₛ (⋃₀ s) = ⨆ t, ⨆ h, supₛ t