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 α, OrderBot α : 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_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sSup : Set α → α
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• 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.

@[reducible]

def CompletePartialOrder.ofLubOfDirected (α : Type u_4) [H1 : PartialOrder α] [H2 : SupSet α] (lub_of_directed : ∀ (d : Set α), DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → IsLUB d (sSup d)) : CompletePartialOrder α

Create a CompletePartialOrder from a PartialOrder and SupSet such that for every directed set d, sSup d is the least upper bound of d.

The bottom element is defined as sSup ∅.

Equations

• CompletePartialOrder.ofLubOfDirected α lub_of_directed = { toPartialOrder := H1, toSupSet := H2, bot := sSup ∅, bot_le := ⋯, lubOfDirected := lub_of_directed }

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.

@[implicit_reducible, instance 100]

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

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

Equations

• CompletePartialOrder.toOmegaCompletePartialOrder = { toPartialOrder := inst✝.toPartialOrder, ωSup := fun (c : OmegaCompletePartialOrder.Chain α) => ⨆ (n : ℕ), c n, le_ωSup := ⋯, ωSup_le := ⋯ }

@[implicit_reducible, instance 100]

instance instConditionallyCompletePartialOrderSup {α : Type u_2} [CompletePartialOrder α] : ConditionallyCompletePartialOrderSup α

A complete partial order is an conditionally complete partial order.

Equations

• instConditionallyCompletePartialOrderSup = { toPartialOrder := inst✝.toPartialOrder, toSupSet := inst✝.toSupSet, isLUB_csSup_of_directed := ⋯ }

@[implicit_reducible, instance 100]

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

A complete lattice is a complete partial order.

Equations

• One or more equations did not get rendered due to their size.