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.

References

• [B. A. Davey and H. A. Priestley, Introduction to lattices and order][davey_priestley]

Tags

complete partial order, directedly complete partial order

class CompletePartialOrder (α : Type u_4) extends PartialOrder , SupSet : 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• sSup : Set α → α
• lubOfDirected : ∀ (d : Set α), DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → IsLUB d (sSup d)

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

theorem CompletePartialOrder.lubOfDirected {α : Type u_4} [self : CompletePartialOrder α] (d : Set α) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → IsLUB d (sSup d)

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

theorem DirectedOn.isLUB_sSup {α : Type u_2} [CompletePartialOrder α] {d : Set α} : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → IsLUB d (sSup d)

theorem DirectedOn.le_sSup {α : Type u_2} [CompletePartialOrder α] {d : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d) (ha : a ∈ d) : a ≤ sSup d

theorem DirectedOn.sSup_le {α : Type u_2} [CompletePartialOrder α] {d : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d) (ha : ∀ b ∈ d, b ≤ a) : sSup d ≤ a

theorem Directed.le_iSup {ι : Sort u_1} {α : Type u_2} [CompletePartialOrder α] {f : ι → α} (hf : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) (i : ι) : f i ≤ ⨆ (j : ι), f j

theorem Directed.iSup_le {ι : Sort u_1} {α : Type u_2} [CompletePartialOrder α] {f : ι → α} {a : α} (hf : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) (ha : ∀ (i : ι), f i ≤ a) : ⨆ (i : ι), f i ≤ a

theorem CompletePartialOrder.scottContinuous {α : Type u_2} {β : Type u_3} [CompletePartialOrder α] [Preorder β] {f : α → β} : ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))

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

instance CompletePartialOrder.toOmegaCompletePartialOrder {α : Type u_2} [CompletePartialOrder α] : OmegaCompletePartialOrder α

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

Equations

• CompletePartialOrder.toOmegaCompletePartialOrder = OmegaCompletePartialOrder.mk (fun (c : OmegaCompletePartialOrder.Chain α) => ⨆ (n : ℕ), c n) ⋯ ⋯

instance CompleteLattice.toCompletePartialOrder {α : Type u_2} [CompleteLattice α] : CompletePartialOrder α

A complete lattice is a complete partial order.

Equations

• CompleteLattice.toCompletePartialOrder = CompletePartialOrder.mk ⋯