refactor(Order): make CompletePartialOrder extend OrderBot

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.

Author: spanning-tree

Mathlib/Order/CompletePartialOrder.lean

@@ -6,6 +6,7 @@ Authors: Christopher Hoskin
 module
 
 public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.BoundedOrder.Basic
 
 /-!
 # Complete Partial Orders
@@ -41,10 +42,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 ∅`.
+-/
+def completePartialOrderOfLubOfDirected (α : 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 (∅ : Set α) (by simp only [DirectedOn,
+    Set.mem_empty_iff_false, false_and, exists_const, imp_self, implies_true])))
+  lubOfDirected := lub_of_directed
+
 variable [CompletePartialOrder α] [Preorder β] {f : ι → α} {d : Set α} {a : α}
 
 protected lemma DirectedOn.isLUB_sSup : DirectedOn (· ≤ ·) d → IsLUB d (sSup d) :=