Lemma pointwiselub_islubpointwise {D D' : dcpo} {I : UU} (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) : ∏ (d : D), islub (pointwisefamily F d) (pointwiselub F isdirec d). Proof. intro d. set (ptfamdir := pointwisefamily_isdirected F isdirec d). exact (make_dcpo_lub_islub ptfamdir). Qed.
Require Import UniMath.Foundations.All.