Complete Partial Orders #
This file considers complete partial orders (sometimes called directedly complete partial orders). These are partial orders for which every directed set has a least upper bound.
Main declarations #
CompletePartialOrder: Typeclass for (directly) complete partial orders.
Main statements #
CompletePartialOrder.toOmegaCompletePartialOrder: A complete partial order is an ω-complete partial order.
CompleteLattice.toCompletePartialOrder: A complete lattice is a complete partial order.
- [B. A. Davey and H. A. Priestley, Introduction to lattices and order][davey_priestley]
complete partial order, directedly complete partial order
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- sSup : Set α → α
For each directed set
sSup dis the least upper bound of
Complete partial orders are partial orders where every directed set has a least upper bound.
Scott-continuity takes on a simpler form in complete partial orders.