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. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.