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. apply is_least_upperbound_dcpo_lub. 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.