Documentation

Mathlib.Order.CompletePartialOrder

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 #

Main statements #

References #

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 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 (x1 x2 : α) => x1 x2) 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 : CompletePartialOrder α] (d : Set α) :
    DirectedOn (fun (x1 x2 : α) => x1 x2) 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} [CompletePartialOrder α] {d : Set α} :
    DirectedOn (fun (x1 x2 : α) => x1 x2) dIsLUB 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 : bd, 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.NonemptyDirectedOn (fun (x1 x2 : α) => x1 x2) 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