The set lattice #
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, x
and⋃₀ s = ⋃ x ∈ s, x
.set.complete_boolean_algebra
:set α
is acomplete_boolean_algebra
with≤ = ⊆
,< = ⊂
,⊓ = ∩
,⊔ = ∪
,⨅ = ⋂
,⨆ = ⋃
and\
as the set difference. Seeset.boolean_algebra
.set.kern_image
: For a functionf : α → β
,s.kern_image f
is the set ofy
such thatf ⁻¹ y ⊆ s
.set.seq
: Union of the image of a set under a sequence of functions.seq s t
is the union off '' t
over allf ∈ s
, wheret : set α
ands : set (α → β)
.set.Union_eq_sigma_of_disjoint
: Equivalence between⋃ i, t i
andΣ i, t i
, wheret
is an indexed family of disjoint sets.
Naming convention #
In lemma names,
⋃ i, s i
is calledUnion
⋂ i, s i
is calledInter
⋃ i j, s i j
is calledUnion₂
. This is aUnion
inside aUnion
.⋂ i j, s i j
is calledInter₂
. This is anInter
inside anInter
.⋃ i ∈ s, t i
is calledbUnion
for "boundedUnion
". This is the special case ofUnion₂
wherej : i ∈ s
.⋂ i ∈ s, t i
is calledbInter
for "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
Indexed intersection of a family of sets
Instances for set.Inter
Instances for ↥set.Inter
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 := _}
set.image
is monotone. See set.image_image
for the statement in terms of ⊆
.
Quantifying over a set is antitone in the set
kern_image f s
is the set of y
such that f ⁻¹ y ⊆ s
.
Equations
- set.kern_image f s = {y : β | ∀ ⦃x : α⦄, f x = y → x ∈ s}
Union and intersection over an indexed family of sets #
An equality version of this lemma is Union_Inter_of_monotone
in data.set.finite
.
Unions and intersections indexed by Prop
#
Bounded unions and intersections #
maps_to
#
restrict_preimage
#
Alias of set.restrict_preimage_injective
.
Alias of set.restrict_preimage_surjective
.
Alias of set.restrict_preimage_bijective
.
inj_on
#
surj_on
#
bij_on
#
image
, preimage
#
The set.image2
version of set.image_eq_Union
Disjoint sets #
We define some lemmas in the disjoint
namespace to be able to use projection notation.
Alias of the reverse direction of set.not_disjoint_iff_nonempty_inter
.
Intervals #
If t
is an indexed family of sets, then there is a natural map from Σ i, t i
to ⋃ i, t i
sending ⟨i, x⟩
to x
.
Equations
- set.sigma_to_Union t x = ⟨↑(x.snd), _⟩
Equivalence between a disjoint union and a dependent sum.
Equations
A set s
is sup-closed if for all x₁, x₂ ∈ s
, x₁ ⊔ x₂ ∈ s
.