proposition: Proposition prod_dcpo_lub {X Y : dcpo} (D : directed_set (X × Y)) : ⨆ D = (⨆ (π₁ {{ D }}) ,, ⨆ (π₂ {{ D }})).
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal