proposition: Proposition dcpo_lub_is_least {X : dcpo} (D : directed_set X) (x : X) (H : ∏ (i : D), D i ⊑ x) : ⨆ D ⊑ x.
proof: Proof. exact (is_least_upperbound_is_least (is_least_upperbound_dcpo_lub D) x H). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets