Definition make_dcpo_is_least_upperbound {X : dcpo} (D : directed_set X) (x : X) (H₁ : ∏ (i : D), D i ⊑ x) (H₂ : ∏ (x' : X), (∏ (i : D), D i ⊑ x') → x ⊑ x') : is_least_upperbound X D x.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.