Compactness properties for complete lattices #
For complete lattices, there are numerous equivalent ways to express the fact that the relation
is well-founded. In this file we define three especially-useful characterisations and provide
proofs that they are indeed equivalent to well-foundedness.
Main definitions #
Main results #
The main result is that the following four conditions are equivalent for a complete lattice:
∀ k, complete_lattice.is_compact_element k
This is demonstrated by means of the following four lemmas:
We also show well-founded lattices are compactly generated
complete lattice, well-founded, compact
A compactness property for a complete lattice is that any
sup-closed non-empty subset
A compactness property for a complete lattice is that any subset has a finite subset with the
k of a complete lattice is said to be compact if any set with
k has a finite subset with
k. Such an element is also called
"finite" or "S-compact".
k is compact if and only if any directed set with
k already got above
k at some point in the set.
A compact element
k has the property that any directed set lying strictly below
its Sup strictly below
- exists_Sup_eq : ∀ (x : α), ∃ (s : set α), (∀ (x : α), x ∈ s → complete_lattice.is_compact_element x) ∧ Sup s = x
A complete lattice is said to be compactly generated if any
element is the
Sup of compact elements.