proposition: Proposition lub_is_monotone {X Y : dcpo} (D : directed_set (funset_dcpo X Y)) (HD : ∏ (d : D), is_monotone X Y (D d)) : is_monotone X Y (⨆ D).
proof: Proof. intros x y p. use dcpo_lub_is_least. intro d ; cbn in d ; cbn. use less_than_dcpo_lub. { exact d. } cbn. apply HD. exact p. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Examples.Propositions UniMath.OrderTheory.DCPOs.Examples.SubDCPO