Lemma islub_islubpointwise {D D' : dcpo} {I : UU} {g : posetofdcpomorphisms D D'} {F : I -> posetofdcpomorphisms D D'} (isdirec : isdirected F) : islub F g -> ∏ (d : D), islub (pointwisefamily F d) (pr1 g d). Proof. intros islubFg d. set (ptlub := make_dcpomorphism (pointwiselub F isdirec) (pointwiselub_isdcpomorphism' F isdirec)). assert (lubeq : g = ptlub). { apply (lubsareunique F islubFg). apply pointwiselub_islub. } rewrite lubeq. apply pointwiselub_islubpointwise. Qed.
Require Import UniMath.Foundations.All.