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. apply maponpaths. apply maponpaths_2. apply eq_monotone_function. exact H. Qed.
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.