proposition: Proposition dcpo_lub_eq_pointwise {X Y : dcpo} (f f' : monotone_function X Y) (D : directed_set X) (H : ∏ (x : X), f x = f' x) : ⨆_{D} f = ⨆_{D} f'.
proof: Proof. apply maponpaths. apply maponpaths_2. apply eq_monotone_function. exact H. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets