refactor(Order): make CompletePartialOrder extend OrderBot (#34477)

Make `CompletePartialOrder` extend `OrderBot`, and add a constructor `completePartialOrderOfLubOfDirected`. Previously, `CompletePartialOrder` had an implicit bottom element but did not extend OrderBot explicitly.

Breaking change: `CompletePartialOrder` instances must provide `⊥` and `bot_le`, or use the constructor.

See discussion in [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.3E.20complete.20partial.20order.20and.20domain.20theory.20formalization).

Author: spanning-tree

Mathlib/Order/CompletePartialOrder.lean

@@ -5,6 +5,7 @@ Authors: Christopher Hoskin
 -/
 module
 
+public import Mathlib.Order.BoundedOrder.Basic
 public import Mathlib.Order.OmegaCompletePartialOrder
 public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 
@@ -42,10 +43,24 @@ section CompletePartialOrder
 /--
 Complete partial orders are partial orders where every directed set has a least upper bound.
 -/
-class CompletePartialOrder (α : Type*) extends PartialOrder α, SupSet α where
+class CompletePartialOrder (α : Type*) extends PartialOrder α, SupSet α, OrderBot α where
   /-- For each directed set `d`, `sSup d` is the least upper bound of `d`. -/
   lubOfDirected : ∀ d, DirectedOn (· ≤ ·) d → IsLUB d (sSup d)
 
+/-- 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 ∅`.
+-/
+@[reducible]
+def CompletePartialOrder.ofLubOfDirected (α : Type*) [H1 : PartialOrder α] [H2 : SupSet α]
+    (lub_of_directed : ∀ d : Set α, DirectedOn (· ≤ ·) d → IsLUB d (sSup d)) :
+    CompletePartialOrder α where
+  __ := H1; __ := H2
+  bot := sSup ∅
+  bot_le := isLUB_empty_iff.mp <| lub_of_directed ∅ IsChain.empty.directedOn
+  lubOfDirected := lub_of_directed
+
 variable [CompletePartialOrder α] [Preorder β] {f : ι → α} {d : Set α} {a : α}
 
 protected lemma DirectedOn.isLUB_sSup : DirectedOn (· ≤ ·) d → IsLUB d (sSup d) :=