proposition: Proposition is_least_upperbound_dcpo_comp_lub {X Y : dcpo} (f : monotone_function X Y) (D : directed_set X) : is_least_upperbound Y (f{{D}}) (⨆_{ D } f).
proof: Proof. apply is_least_upperbound_dcpo_lub. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets