Lemma pointwiselub_islub {D D' : dcpo} {I : UU} (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) : islub F (make_dcpomorphism (pointwiselub F isdirec) (pointwiselub_isdcpomorphism' F isdirec)). Proof. split. - intro i; simpl. intro d; simpl. apply pointwiselub_islubpointwise. - intros h ineqs; simpl. intro d; simpl. apply pointwiselub_islubpointwise. intro i. use (ineqs i). Qed.
Require Import UniMath.Foundations.All.