The set lattice #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides usual set notation for unions and intersections, a complete_lattice instance
for set α, and some more set constructions.
Main declarations #
set.Union: Union of an indexed family of sets.set.Inter: Intersection of an indexed family of sets.set.sInter: set Inter. Intersection of sets belonging to a set of sets.set.sUnion: set Union. Union of sets belonging to a set of sets. This is actually defined in core Lean.set.sInter_eq_bInter,set.sUnion_eq_bInter: Shows that⋂₀ s = ⋂ x ∈ s, xand⋃₀ s = ⋃ x ∈ s, x.set.complete_boolean_algebra:set αis acomplete_boolean_algebrawith≤ = ⊆,< = ⊂,⊓ = ∩,⊔ = ∪,⨅ = ⋂,⨆ = ⋃and\as the set difference. Seeset.boolean_algebra.set.kern_image: For a functionf : α → β,s.kern_image fis the set ofysuch thatf ⁻¹ y ⊆ s.set.seq: Union of the image of a set under a sequence of functions.seq s tis the union off '' tover allf ∈ s, wheret : set αands : set (α → β).set.Union_eq_sigma_of_disjoint: Equivalence between⋃ i, t iandΣ i, t i, wheretis an indexed family of disjoint sets.
Naming convention #
In lemma names,
⋃ i, s iis calledUnion⋂ i, s iis calledInter⋃ i j, s i jis calledUnion₂. This is aUnioninside aUnion.⋂ i j, s i jis calledInter₂. This is anInterinside anInter.⋃ i ∈ s, t iis calledbUnionfor "boundedUnion". This is the special case ofUnion₂wherej : i ∈ s.⋂ i ∈ s, t iis calledbInterfor "boundedInter". This is the special case ofInter₂wherej : i ∈ s.
Notation #
⋃:set.Union⋂:set.Inter⋃₀:set.sUnion⋂₀:set.sInter
Complete lattice and complete Boolean algebra instances #
Intersection of a set of sets.
Equations
- ⋂₀ S = has_Inf.Inf S
Indexed union of a family of sets
Instances for ↥set.Union
@[protected, instance]
Equations
- set.complete_boolean_algebra = {sup := boolean_algebra.sup set.boolean_algebra, le := boolean_algebra.le set.boolean_algebra, lt := boolean_algebra.lt set.boolean_algebra, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := boolean_algebra.inf set.boolean_algebra, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := boolean_algebra.compl set.boolean_algebra, sdiff := boolean_algebra.sdiff set.boolean_algebra, himp := boolean_algebra.himp set.boolean_algebra, top := boolean_algebra.top set.boolean_algebra, bot := boolean_algebra.bot set.boolean_algebra, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _, Sup := has_Sup.Sup set.has_Sup, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf set.has_Inf, Inf_le := _, le_Inf := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}
@[protected]
theorem
set.image_preimage
{α : Type u_1}
{β : Type u_2}
{f : α → β} :
galois_connection (set.image f) (set.preimage f)
@[protected]
Union and intersection over an indexed family of sets #
theorem
set.directed_on_Union
{α : Type u_1}
{ι : Sort u_4}
{r : α → α → Prop}
{f : ι → set α}
(hd : directed has_subset.subset f)
(h : ∀ (x : ι), directed_on r (f x)) :
directed_on r (⋃ (x : ι), f x)
Unions and intersections indexed by Prop #
Bounded unions and intersections #
maps_to #
theorem
set.maps_to_sUnion
{α : Type u_1}
{β : Type u_2}
{S : set (set α)}
{t : set β}
{f : α → β}
(H : ∀ (s : set α), s ∈ S → set.maps_to f s t) :
set.maps_to f (⋃₀ S) t
theorem
set.maps_to_Union
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → set α}
{t : set β}
{f : α → β}
(H : ∀ (i : ι), set.maps_to f (s i) t) :
set.maps_to f (⋃ (i : ι), s i) t
theorem
set.maps_to_sInter
{α : Type u_1}
{β : Type u_2}
{s : set α}
{T : set (set β)}
{f : α → β}
(H : ∀ (t : set β), t ∈ T → set.maps_to f s t) :
set.maps_to f s (⋂₀ T)
theorem
set.maps_to_Inter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : set α}
{t : ι → set β}
{f : α → β}
(H : ∀ (i : ι), set.maps_to f s (t i)) :
set.maps_to f s (⋂ (i : ι), t i)
restrict_preimage #
theorem
set.injective_iff_injective_of_Union_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{U : ι → set β}
(hU : set.Union U = set.univ) :
function.injective f ↔ ∀ (i : ι), function.injective ((U i).restrict_preimage f)
theorem
set.surjective_iff_surjective_of_Union_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{U : ι → set β}
(hU : set.Union U = set.univ) :
function.surjective f ↔ ∀ (i : ι), function.surjective ((U i).restrict_preimage f)
theorem
set.bijective_iff_bijective_of_Union_eq_univ
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{f : α → β}
{U : ι → set β}
(hU : set.Union U = set.univ) :
function.bijective f ↔ ∀ (i : ι), function.bijective ((U i).restrict_preimage f)
inj_on #
theorem
set.inj_on_Union_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → set α}
(hs : directed has_subset.subset s)
{f : α → β}
(hf : ∀ (i : ι), set.inj_on f (s i)) :
set.inj_on f (⋃ (i : ι), s i)
surj_on #
theorem
set.surj_on_sUnion
{α : Type u_1}
{β : Type u_2}
{s : set α}
{T : set (set β)}
{f : α → β}
(H : ∀ (t : set β), t ∈ T → set.surj_on f s t) :
set.surj_on f s (⋃₀ T)
theorem
set.surj_on_Union
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : set α}
{t : ι → set β}
{f : α → β}
(H : ∀ (i : ι), set.surj_on f s (t i)) :
set.surj_on f s (⋃ (i : ι), t i)
theorem
set.surj_on_Inter
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[hi : nonempty ι]
{s : ι → set α}
{t : set β}
{f : α → β}
(H : ∀ (i : ι), set.surj_on f (s i) t)
(Hinj : set.inj_on f (⋃ (i : ι), s i)) :
set.surj_on f (⋂ (i : ι), s i) t
bij_on #
theorem
set.bij_on_Union
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → set α}
{t : ι → set β}
{f : α → β}
(H : ∀ (i : ι), set.bij_on f (s i) (t i))
(Hinj : set.inj_on f (⋃ (i : ι), s i)) :
set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem
set.bij_on_Union_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{s : ι → set α}
(hs : directed has_subset.subset s)
{t : ι → set β}
{f : α → β}
(H : ∀ (i : ι), set.bij_on f (s i) (t i)) :
set.bij_on f (⋃ (i : ι), s i) (⋃ (i : ι), t i)
theorem
set.bij_on_Inter_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[nonempty ι]
{s : ι → set α}
(hs : directed has_subset.subset s)
{t : ι → set β}
{f : α → β}
(H : ∀ (i : ι), set.bij_on f (s i) (t i)) :
set.bij_on f (⋂ (i : ι), s i) (⋂ (i : ι), t i)
image, preimage #
theorem
set.image2_eq_Union
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : set α)
(t : set β) :
The set.image2 version of set.image_eq_Union
Given a set s of functions α → β and t : set α, seq s t is the union of f '' t over
all f ∈ s.
Instances for ↥set.seq
Disjoint sets #
We define some lemmas in the disjoint namespace to be able to use projection notation.
Intervals #
theorem
Sup_sUnion
{β : Type u_2}
[complete_lattice β]
(s : set (set β)) :
has_Sup.Sup (⋃₀ s) = ⨆ (t : set β) (H : t ∈ s), has_Sup.Sup t
theorem
Inf_sUnion
{β : Type u_2}
[complete_lattice β]
(s : set (set β)) :
has_Inf.Inf (⋃₀ s) = ⨅ (t : set β) (H : t ∈ s), has_Inf.Inf t