Definition sub_dcpo_lub (D : directed_set (sub_PartialOrder X P)) : lub (sub_PartialOrder X P) D. Proof. pose (D' := directed_set_comp (pr1_sub_monotone X P) D). use make_lub. - refine (⨆ D' ,, HP D' _). abstract (intro d ; exact (pr2 (D d))). - split. + abstract (intro i ; cbn ; exact (less_than_dcpo_lub D' (pr1 (D i)) i (refl_dcpo _))). + abstract (intros x Hx ; use (dcpo_lub_is_least D') ; intro i ; apply (Hx i)). Defined.
Require Import UniMath.Foundations.All. 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. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.