Proposition pr2_is_least_upperbound {X Y : hSet} {DX : dcpo_struct X} {DY : dcpo_struct Y} {I : UU} {D : I → X × Y} (xy : X × Y) (Hxy : is_least_upperbound (prod_dcpo_struct DX DY) D xy) : is_least_upperbound DY (λ i, pr2 (D i)) (pr2 xy). Proof. split. - intros i. exact (pr2 (is_least_upperbound_is_upperbound Hxy i)). - intros y Hy. refine (pr2 (is_least_upperbound_is_least Hxy (pr1 xy ,, y) _)). intros i. split ; cbn. + exact (pr1 (is_least_upperbound_is_upperbound Hxy i)). + exact (Hy i). 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.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.