Proposition dcpo_lub_is_least {X : dcpo} (D : directed_set X) (x : X) (H : ∏ (i : D), D i ⊑ x) : ⨆ D ⊑ x. Proof. exact (is_least_upperbound_is_least (is_least_upperbound_dcpo_lub D) x H). Qed.
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.