Lemma pointwiselub_preservesorder {D D' : dcpo} {I : UU} (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) : isaposetmorphism (pointwiselub F isdirec). Proof. intros x y ineq. use lubpreservesorder. - exact I. - intro i. apply (F i). exact x. - intro i. apply (F i). exact y. - intro i. simpl. apply dcpomorphism_preservesorder. exact ineq. - simpl. apply pointwiselub_islubpointwise. - simpl. apply pointwiselub_islubpointwise. Qed.
Require Import UniMath.Foundations.All.