Proposition is_monotone_pointwise_lub (x₁ x₂ : X) (p : x₁ ⊑ x₂) : pointwise_lub x₁ ⊑ pointwise_lub x₂. Proof. unfold pointwise_lub. use dcpo_lub_is_least ; cbn. intro i. use less_than_dcpo_lub. - exact i. - exact (is_monotone_scott_continuous_map (_ ,, pr2 (D i)) p). Qed.
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. Require Import UniMath.OrderTheory.DCPOs.Core.FubiniTheorem. Require Import UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.