feat: define ConditionallyCompletePartialOrder (#35046)

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.

Author: j-loreaux

Mathlib.lean

@@ -5570,6 +5570,7 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompleteLattice.Finset
 public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover

Mathlib/Order/ConditionallyCompletePartialOrder/Defs.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Order.Bounds.Defs
+public import Mathlib.Order.Directed
+public import Mathlib.Order.SetNotation
+
+/-! # 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.
+
+-/
+
+@[expose] public section
+
+variable {ι : Sort*} {α : Type*}
+
+/-- Conditionally complete partial orders (with infima) are partial orders
+where every nonempty, directed set which is bounded below has a greatest lower bound. -/
+class ConditionallyCompletePartialOrderInf (α : Type*)
+    extends PartialOrder α, InfSet α where
+  /-- For each nonempty, directed set `s` which is bounded below, `sInf s` is
+  the greatest lower bound of `s`. -/
+  isGLB_csInf_of_directed :
+    ∀ s, DirectedOn (· ≥ ·) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)
+
+/-- Conditionally complete partial orders (with suprema) are partial orders
+where every nonempty, directed set which is bounded above has a least upper bound. -/
+@[to_dual existing]
+class ConditionallyCompletePartialOrderSup (α : Type*)
+    extends PartialOrder α, SupSet α where
+  /-- For each nonempty, directed set `s` which is bounded above, `sSup s` is
+  the least upper bound of `s`. -/
+  isLUB_csSup_of_directed :
+    ∀ s, DirectedOn (· ≤ ·) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)
+
+/-- 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. -/
+class ConditionallyCompletePartialOrder (α : Type*)
+    extends ConditionallyCompletePartialOrderSup α, ConditionallyCompletePartialOrderInf α where
+
+variable [ConditionallyCompletePartialOrderSup α]
+variable {f : ι → α} {s : Set α} {a : α}
+
+@[to_dual]
+protected lemma DirectedOn.isLUB_csSup (h_dir : DirectedOn (· ≤ ·) s)
+    (h_non : s.Nonempty) (h_bdd : BddAbove s) : IsLUB s (sSup s) :=
+  ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed s h_dir h_non h_bdd
+
+@[to_dual csInf_le]
+protected lemma DirectedOn.le_csSup (hs : DirectedOn (· ≤ ·) s)
+    (h_bdd : BddAbove s) (ha : a ∈ s) : a ≤ sSup s :=
+  (hs.isLUB_csSup ⟨a, ha⟩ h_bdd).1 ha
+
+@[to_dual le_csInf]
+protected lemma DirectedOn.csSup_le (hd : DirectedOn (· ≤ ·) s) (h_non : s.Nonempty)
+    (ha : ∀ b ∈ s, b ≤ a) : sSup s ≤ a :=
+  (hd.isLUB_csSup h_non ⟨a, ha⟩).2 ha
+
+@[to_dual ciInf_le]
+protected lemma Directed.le_ciSup (hf : Directed (· ≤ ·) f)
+    (hf_bdd : BddAbove (Set.range f)) (i : ι) : f i ≤ ⨆ j, f j :=
+  hf.directedOn_range.le_csSup  hf_bdd <| Set.mem_range_self _
+
+@[to_dual le_ciInf]
+protected lemma Directed.ciSup_le [Nonempty ι] (hf : Directed (· ≤ ·) f)
+    (ha : ∀ i, f i ≤ a) : ⨆ i, f i ≤ a :=
+  hf.directedOn_range.csSup_le (Set.range_nonempty _) <| Set.forall_mem_range.2 ha