Conditionally complete partial orders

This file defines conditionally complete partial orders with suprema, infima or both. These are partial orders where every nonempty, upwards (downwards) directed set which is bounded above (below) has a least upper bound (greatest lower bound). This class extends SupSet (InfSet) and the requirement is that sSup (sInf) must be the least upper bound.

The three classes defined herein are:

• ConditionallyCompletePartialOrderSup for partial orders with suprema,
• ConditionallyCompletePartialOrderInf for partial orders with infima, and
• ConditionallyCompletePartialOrder for partial orders with both suprema and infima

One common use case for these classes is the order on a von Neumann algebra, or W⋆-algebra. This is the strongest order-theoretic structure satisfied by a von Neumann algebra; in particular it is not a conditionally complete lattice, and indeed it is a lattice if and only if the algebra is commutative. In addition, ℂ can be made to satisfy this class (one must provide a suitable SupSet instance), with the order w ≤ z ↔ w.re ≤ z.re ∧ w.im = z.im, which is available in the ComplexOrder namespace.

These use cases are the motivation for defining three classes, as compared with other parts of the order theory library, where only the supremum versions are defined (e.g., CompletePartialOrder and OmegaCompletePartialOrder). We note that, if these classes are used outside of order theory, then it is more likely that the infimum versions would be useful. Indeed, whenever the underlying type has an antitone involution (e.g., if it is an ordered ring, then negation would be such a map), then any ConditionallyCompletePartialOrder{Sup,Inf} is automatically a ConditionallyCompletePartialOrder. Because of the to_dual attribute, the additional overhead required to add and maintain the infimum version is minimal.

class ConditionallyCompletePartialOrderInf (α : Type u_3) extends PartialOrder α, InfSet α : Type u_3

Conditionally complete partial orders (with infima) are partial orders where every nonempty, directed set which is bounded below has a greatest lower 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
• sInf : Set α → α
• isGLB_csInf_of_directed (s : Set α) : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)

  For each nonempty, directed set s which is bounded below, sInf s is the greatest lower bound of s.

class ConditionallyCompletePartialOrderSup (α : Type u_3) extends PartialOrder α, SupSet α : Type u_3

Conditionally complete partial orders (with suprema) are partial orders where every nonempty, directed set which is bounded above 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 α → α
• isLUB_csSup_of_directed (s : Set α) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)

  For each nonempty, directed set s which is bounded above, sSup s is the least upper bound of s.

class ConditionallyCompletePartialOrder (α : Type u_3) extends ConditionallyCompletePartialOrderSup α, ConditionallyCompletePartialOrderInf α : Type u_3

Conditionally complete partial orders (with suprema and infimae) are partial orders where every nonempty, directed set which is bounded above (respectively, below) has a least upper (respectively, greatest lower) 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 α → α
• isLUB_csSup_of_directed (s : Set α) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)
• sInf : Set α → α
• isGLB_csInf_of_directed (s : Set α) : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)

theorem DirectedOn.isLUB_csSup {α : Type u_2} [ConditionallyCompletePartialOrderSup α] {s : Set α} (h_dir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (h_non : s.Nonempty) (h_bdd : BddAbove s) : IsLUB s (sSup s)

theorem DirectedOn.isGLB_csInf {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {s : Set α} (h_dir : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (h_non : s.Nonempty) (h_bdd : BddBelow s) : IsGLB s (sInf s)

theorem DirectedOn.le_csSup {α : Type u_2} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (hs : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (h_bdd : BddAbove s) (ha : a ∈ s) : a ≤ sSup s

theorem DirectedOn.csInf_le {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hs : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (h_bdd : BddBelow s) (ha : a ∈ s) : sInf s ≤ a

theorem DirectedOn.csSup_le {α : Type u_2} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (h_non : s.Nonempty) (ha : ∀ b ∈ s, b ≤ a) : sSup s ≤ a

theorem DirectedOn.le_csInf {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (h_non : s.Nonempty) (ha : ∀ b ∈ s, a ≤ b) : a ≤ sInf s

theorem Directed.le_ciSup {ι : Sort u_1} {α : Type u_2} [ConditionallyCompletePartialOrderSup α] {f : ι → α} (hf : Directed (fun (x1 x2 : α) => x1 ≤ x2) f) (hf_bdd : BddAbove (Set.range f)) (i : ι) : f i ≤ ⨆ (j : ι), f j

theorem Directed.ciInf_le {ι : Sort u_1} {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {f : ι → α} (hf : Directed (fun (x1 x2 : α) => x2 ≤ x1) f) (hf_bdd : BddBelow (Set.range f)) (i : ι) : ⨅ (j : ι), f j ≤ f i

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

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