Theory of complete lattices #
This file contains basic results on complete lattices.
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 #
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.
Instances #
Equations
- One or more equations did not get rendered due to their size.
Equations
- Pi.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Prod.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Pullback a CompleteLattice
along an injection.
Equations
- Function.Injective.completeLattice f hf map_sup map_inf map_sSup map_sInf map_top map_bot = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯