Theory of complete lattices #
Main definitions #
supₛ
andinfₛ
are the supremum and the infimum of a set;supᵢ (f : ι → α)→ α)
andinfᵢ (f : ι → α)→ α)
are indexed supremum and infimum of a function, defined assupₛ
andinfₛ
of the range of this function;class CompleteLattice
: a bounded lattice such thatsupₛ s
is always the least upper boundary ofs
andinfₛ s
is always the greatest lower boundary ofs
;class CompleteLinearOrder
: a linear ordered complete lattice.
Naming conventions #
In lemma names,
supₛ
is calledsupₛ
infₛ
is calledinfₛ
⨆ i, s i⨆ i, s i
is calledsupᵢ
⨅ i, s i⨅ i, s i
is calledinfᵢ
⨆ i j, s i j⨆ i j, s i j
is calledsupᵢ₂
. This is asupᵢ
inside asupᵢ
.⨅ i j, s i j⨅ i j, s i j
is calledinfᵢ₂
. This is aninfᵢ
inside aninfᵢ
.⨆ i ∈ s, t i⨆ i ∈ s, t i∈ s, t i
is calledbsupᵢ
for "boundedsupᵢ
". This is the special case ofsupᵢ₂
wherej : i ∈ s∈ s
.⨅ i ∈ s, t i⨅ i ∈ s, t i∈ s, t i
is calledbinfᵢ
for "boundedinfᵢ
". This is the special case ofinfᵢ₂
wherej : i ∈ s∈ s
.
Notation #
⨆ i, f i⨆ i, f i
:supᵢ f
, the supremum of the range off
;⨅ i, f i⨅ i, f i
:infᵢ f
, the infimum of the range off
.
Indexed supremum.
Equations
- One or more equations did not get rendered due to their size.
Unexpander for the indexed supremum notation.
Equations
- One or more equations did not get rendered due to their size.
Indexed infimum.
Equations
- One or more equations did not get rendered due to their size.
Unexpander for the indexed infimum notation.
Equations
- One or more equations did not get rendered due to their size.
Equations
- OrderDual.supSet α = { supₛ := infₛ }
Equations
- OrderDual.infSet α = { infₛ := supₛ }
Any element of a set is less than the set supremum.
Any upper bound is more than the set supremum.
Note that we rarely use CompleteSemilatticeSup
(in fact, any such object is always a CompleteLattice
, so it's usually best to start there).
Nevertheless it is sometimes a useful intermediate step in constructions.
Instances
Any element of a set is more than the set infimum.
Any lower bound is less than the set infimum.
Note that we rarely use CompleteSemilatticeInf
(in fact, any such object is always a CompleteLattice
, so it's usually best to start there).
Nevertheless it is sometimes a useful intermediate step in constructions.
Instances
Equations
- CompleteLattice.toBoundedOrder = BoundedOrder.mk
Create a CompleteLattice
from a PartialOrder
and InfSet
that returns the greatest lower bound of a set. Usually this constructor provides
poor definitional equalities. If other fields are known explicitly, they should be
provided; for example, if inf
is known explicitly, construct the CompleteLattice
instance as
instance : CompleteLattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, supₛ, bot, top
..completeLatticeOfInf my_T _ }
Equations
- One or more equations did not get rendered due to their size.
Any CompleteSemilatticeInf
is in fact a CompleteLattice
.
Note that this construction has bad definitional properties:
see the doc-string on completeLatticeOfInf
.
Equations
- completeLatticeOfCompleteSemilatticeInf α = completeLatticeOfInf α (_ : ∀ (s : Set α), IsGLB s (infₛ s))
Create a CompleteLattice
from a PartialOrder
and SupSet
that returns the least upper bound of a set. Usually this constructor provides
poor definitional equalities. If other fields are known explicitly, they should be
provided; for example, if inf
is known explicitly, construct the CompleteLattice
instance as
instance : CompleteLattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, infₛ, bot, top
..completeLatticeOfSup my_T _ }
Equations
- One or more equations did not get rendered due to their size.
Any CompleteSemilatticeSup
is in fact a CompleteLattice
.
Note that this construction has bad definitional properties:
see the doc-string on completeLatticeOfSup
.
Equations
- completeLatticeOfCompleteSemilatticeSup α = completeLatticeOfSup α (_ : ∀ (s : Set α), IsLUB s (supₛ s))
A linear order is total.
In a linearly ordered type, we assume the order relations are all decidable.
decidable_le : DecidableRel fun x x_1 => x ≤ x_1In a linearly ordered type, we assume the order relations are all decidable.
decidable_eq : DecidableEq αIn a linearly ordered type, we assume the order relations are all decidable.
decidable_lt : DecidableRel fun x x_1 => x < x_1
A complete linear order is a linear order whose lattice structure is complete.
Instances
Equations
- CompleteLinearOrder.toLinearOrder = LinearOrder.mk (_ : ∀ (a b : α), a ≤ b ∨ b ≤ a) CompleteLinearOrder.decidable_le CompleteLinearOrder.decidable_eq CompleteLinearOrder.decidable_lt
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.
Introduction rule to prove that b
is the supremum of s
: it suffices to check that b
is larger than all elements of s
, and that this is not the case of any w < b
.
See csupₛ_eq_of_forall_le_of_forall_lt_exists_gt
for a version in conditionally complete
lattices.
Introduction rule to prove that b
is the infimum of s
: it suffices to check that b
is smaller than all elements of s
, and that this is not the case of any w > b
.
See cinfₛ_eq_of_forall_ge_of_forall_gt_exists_lt
for a version in conditionally complete
lattices.
Introduction rule to prove that b
is the supremum of f
: it suffices to check that b
is larger than f i
for all i
, and that this is not the case of any w.
See
csupᵢ_eq_of_forall_le_of_forall_lt_exists_gt
for a version in conditionally complete
lattices.
Introduction rule to prove that b
is the infimum of f
: it suffices to check that b
is smaller than f i
for all i
, and that this is not the case of any w>b
.
See cinfᵢ_eq_of_forall_ge_of_forall_gt_exists_lt
for a version in conditionally complete
lattices.
A version of supᵢ_option
useful for rewriting right-to-left.
A version of infᵢ_option
useful for rewriting right-to-left.
When taking the supremum of f : ι → α→ α
, the elements of ι
on which f
gives ⊥⊥
can be
dropped, without changing the result.
When taking the infimum of f : ι → α→ α
, the elements of ι
on which f
gives ⊤⊤
can be
dropped, without changing the result.
Instances #
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.
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.
This is a weaker version of sup_infₛ_eq
This is a weaker version of inf_supₛ_eq
This is a weaker version of infₛ_sup_eq
This is a weaker version of supₛ_inf_eq
Pullback a CompleteLattice
along an injection.
Equations
- One or more equations did not get rendered due to their size.