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 aCompleteBooleanAlgebra
with≤ = ⊆≤ = ⊆⊆
,< = ⊂⊂
,⊓ = ∩⊓ = ∩∩
,⊔ = ∪⊔ = ∪∪
,⨅ = ⋂⨅ = ⋂⋂
,⨆ = ⋃⨆ = ⋃⋃
and\
as the set difference. SeeSet.BooleanAlgebra
.Set.kern_image
: For a functionf : α → β→ β
,s.kern_image f
is the set ofy
such thatf ⁻¹ 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 off '' t
over allf ∈ s∈ s
, wheret : Set α
ands : Set (α → β)→ β)
.Set.unionᵢ_eq_sigma_of_disjoint
: Equivalence between⋃ i, t i⋃ i, t i
andΣ i, t i
, wheret
is an indexed family of disjoint sets.
Naming convention #
In lemma names,
⋃ i, s i⋃ i, s i
is calledunionᵢ
⋂ i, s i⋂ i, s i
is calledinterᵢ
⋃ i j, s i j⋃ i j, s i j
is calledunionᵢ₂
. This is aunionᵢ
inside aunionᵢ
.⋂ i j, s i j⋂ i j, s i j
is calledinterᵢ₂
. This is aninterᵢ
inside aninterᵢ
.⋃ i ∈ s, t i⋃ i ∈ s, t i∈ s, t i
is calledbunionᵢ
for "boundedunionᵢ
". This is the special case ofunionᵢ₂
wherej : i ∈ s∈ s
.⋂ i ∈ s, t i⋂ i ∈ s, t i∈ s, t i
is calledbinterᵢ
for "boundedinterᵢ
". This is the special case ofinterᵢ₂
wherej : i ∈ s∈ s
.
Notation #
⋃⋃
:Set.unionᵢ
⋂⋂
:Set.interᵢ
⋃₀⋃₀
:Set.unionₛ
⋂₀⋂₀
:Set.interₛ
Complete lattice and complete Boolean algebra instances #
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))
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))
Indexed union of a family of sets
Equations
- Set.unionᵢ s = supᵢ s
Indexed intersection of a family of sets
Equations
- Set.interᵢ s = infᵢ s
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.
Equations
- One or more equations did not get rendered due to their size.
Union and intersection over an indexed family of sets #
Equations
- Set.instOrderTopSetInstLESet = OrderTop.mk (_ : ∀ (a : Set α), a ⊆ Set.univ)
This rather trivial consequence of subset_unionᵢ
is convenient with apply
, and has i
explicit for this purpose.
This rather trivial consequence of interᵢ_subset
is convenient with apply
, and has i
explicit for this purpose.
This rather trivial consequence of subset_unionᵢ₂
is convenient with apply
, and has i
and
j
explicit for this purpose.
This rather trivial consequence of interᵢ₂_subset
is convenient with apply
, and has i
and
j
explicit for this purpose.
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 #
A specialization of mem_unionᵢ₂
.
A specialization of mem_interᵢ₂
.
A specialization of subset_unionᵢ₂
.
A specialization of interᵢ₂_subset
.
mapsTo
#
restrictPreimage
#
InjOn
#
SurjOn
#
BijOn
#
image
, preimage
#
The Set.image2
version of Set.image_eq_unionᵢ
Disjoint sets #
Intervals #
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) }
Equivalence between a disjoint union and a dependent sum.