# 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.

## Tags #

complete partial order, directedly complete partial order

class CompletePartialOrder (α : Type u_4) extends , :
Type u_4

Complete partial orders are partial orders where every directed set has a least upper bound.

• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• sSup : Set αα
• lubOfDirected : ∀ (d : Set α), DirectedOn (fun (x x_1 : α) => x x_1) dIsLUB d (sSup d)

For each directed set d, sSup d is the least upper bound of d.

Instances
theorem CompletePartialOrder.lubOfDirected {α : Type u_4} [self : ] (d : Set α) :
DirectedOn (fun (x x_1 : α) => x x_1) dIsLUB d (sSup d)

For each directed set d, sSup d is the least upper bound of d.

theorem DirectedOn.isLUB_sSup {α : Type u_2} {d : Set α} :
DirectedOn (fun (x x_1 : α) => x x_1) dIsLUB d (sSup d)
theorem DirectedOn.le_sSup {α : Type u_2} {d : Set α} {a : α} (hd : DirectedOn (fun (x x_1 : α) => x x_1) d) (ha : a d) :
a sSup d
theorem DirectedOn.sSup_le {α : Type u_2} {d : Set α} {a : α} (hd : DirectedOn (fun (x x_1 : α) => x x_1) d) (ha : bd, b a) :
sSup d a
theorem Directed.le_iSup {ι : Sort u_1} {α : Type u_2} {f : ια} (hf : Directed (fun (x x_1 : α) => x x_1) f) (i : ι) :
f i ⨆ (j : ι), f j
theorem Directed.iSup_le {ι : Sort u_1} {α : Type u_2} {f : ια} {a : α} (hf : Directed (fun (x x_1 : α) => x x_1) f) (ha : ∀ (i : ι), f i a) :
⨆ (i : ι), f i a
theorem CompletePartialOrder.scottContinuous {α : Type u_2} {β : Type u_3} [] {f : αβ} :
∀ ⦃d : Set α⦄, d.NonemptyDirectedOn (fun (x x_1 : α) => x x_1) dIsLUB (f '' d) (f (sSup d))

Scott-continuity takes on a simpler form in complete partial orders.

A complete partial order is an ω-complete partial order.

Equations

A complete lattice is a complete partial order.

Equations
• CompleteLattice.toCompletePartialOrder =