Theory of complete lattices #
Main definitions #
sSup
andsInf
are the supremum and the infimum of a set;iSup (f : ι → α)
andiInf (f : ι → α)
are indexed supremum and infimum of a function, defined assSup
andsInf
of the range of this function;- class
CompleteLattice
: a bounded lattice such thatsSup s
is always the least upper boundary ofs
andsInf s
is always the greatest lower boundary ofs
; - class
CompleteLinearOrder
: a linear ordered complete lattice.
Naming conventions #
In lemma names,
sSup
is calledsSup
sInf
is calledsInf
⨆ i, s i
is callediSup
⨅ i, s i
is callediInf
⨆ i j, s i j
is callediSup₂
. This is aniSup
inside aniSup
.⨅ i j, s i j
is callediInf₂
. This is aniInf
inside aniInf
.⨆ i ∈ s, t i
is calledbiSup
for "boundediSup
". This is the special case ofiSup₂
wherej : i ∈ s
.⨅ i ∈ s, t i
is calledbiInf
for "boundediInf
". This is the special case ofiInf₂
wherej : i ∈ s
.
Notation #
Equations
- OrderDual.supSet α = { sSup := sInf }
Equations
- OrderDual.infSet α = { sInf := sSup }
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.
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- sSup : Set α → α
Any element of a set is less than the set supremum.
Any upper bound is more than the set supremum.
Instances
Alias of the forward direction of isLUB_iff_sSup_eq
.
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.
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- sInf : Set α → α
Any element of a set is more than the set infimum.
Any lower bound is less than the set infimum.
Instances
Alias of the forward direction of isGLB_iff_sInf_eq
.
A complete lattice is a bounded lattice which has suprema and infima for every subset.
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- inf : α → α → α
- sSup : Set α → α
Any element of a set is less than the set supremum.
Any upper bound is more than the set supremum.
- sInf : Set α → α
Any element of a set is more than the set infimum.
Any lower bound is less than the set infimum.
- top : α
- bot : α
Any element is less than the top one.
Any element is more than the bottom one.
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 where
inf := better_inf
le_inf := ...
inf_le_right := ...
inf_le_left := ...
-- don't care to fix sup, sSup, bot, top
__ := completeLatticeOfInf my_T _
Equations
- completeLatticeOfInf α isGLB_sInf = let __spread.0 := H1; let __spread.1 := H2; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Any CompleteSemilatticeInf
is in fact a CompleteLattice
.
Note that this construction has bad definitional properties:
see the doc-string on completeLatticeOfInf
.
Equations
Instances For
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 where
inf := better_inf
le_inf := ...
inf_le_right := ...
inf_le_left := ...
-- don't care to fix sup, sInf, bot, top
__ := completeLatticeOfSup my_T _
Equations
- completeLatticeOfSup α isLUB_sSup = let __spread.0 := H1; let __spread.1 := H2; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Any CompleteSemilatticeSup
is in fact a CompleteLattice
.
Note that this construction has bad definitional properties:
see the doc-string on completeLatticeOfSup
.
Equations
Instances For
A complete linear order is a linear order whose lattice structure is complete.
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- inf : α → α → α
- sSup : Set α → α
- sInf : Set α → α
- top : α
- bot : α
A linear order is total.
- decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
In a linearly ordered type, we assume the order relations are all decidable.
- decidableEq : DecidableEq α
In a linearly ordered type, we assume the order relations are all decidable.
- decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
In a linearly ordered type, we assume the order relations are all decidable.
Instances
Equations
- CompleteLinearOrder.toLinearOrder = let __spread.0 := i; LinearOrder.mk ⋯ CompleteLinearOrder.decidableLE CompleteLinearOrder.decidableEq CompleteLinearOrder.decidableLT ⋯ ⋯ ⋯
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 csSup_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 csInf_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<b
.
See ciSup_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 ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
for a version in conditionally complete
lattices.
A version of iSup_option
useful for rewriting right-to-left.
A version of iInf_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
- Pi.instCompleteLattice = let __spread.0 := Pi.instBoundedOrder; let __spread.1 := Pi.instLattice; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
This is a weaker version of sup_sInf_eq
This is a weaker version of inf_sSup_eq
This is a weaker version of sInf_sup_eq
This is a weaker version of sSup_inf_eq
Pullback a CompleteLattice
along an injection.
Equations
- Function.Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot = let __spread.0 := Function.Injective.lattice f hf map_sup map_inf; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Equations
- ULift.supSet = { sSup := fun (s : Set (ULift.{v, u_1} α)) => { down := sSup (ULift.up ⁻¹' s) } }
Equations
- ULift.infSet = { sInf := fun (s : Set (ULift.{v, u_1} α)) => { down := sInf (ULift.up ⁻¹' s) } }
Equations
- ULift.instCompleteLattice = Function.Injective.completeLattice ULift.down ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯