Proposition prod_dcpo_lub {X Y : dcpo} (D : directed_set (X × Y)) : ⨆ D = (⨆ (π₁ {{ D }}) ,, ⨆ (π₂ {{ D }})). Proof. use (eq_lub (X × Y) D). - apply is_least_upperbound_dcpo_lub. - use is_least_upperbound_pair. + exact (is_least_upperbound_dcpo_comp_lub (dirprod_pr1_scott_continuous_map X Y) D). + exact (is_least_upperbound_dcpo_comp_lub (dirprod_pr2_scott_continuous_map X Y) D). 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.