Definition prod_lub {X Y : hSet} (DX : dcpo_struct X) (DY : dcpo_struct Y) (I : UU) (D : I → (X × Y)%set) (x : lub DX (λ i, pr1 (D i))) (y : lub DY (λ i, pr2 (D i))) : lub (prod_PartialOrder DX DY) D. Proof. use make_lub. - exact (pr1 x ,, pr1 y). - use is_least_upperbound_pair. + exact (pr2 x). + exact (pr2 y). Defined.
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.