Proposition prod_dcpo_lub' {X Y : dcpo} (D : directed_set X) (D' : directed_set Y) : ⨆ (prod_directed_set_dcpo D D') = (⨆ D ,, ⨆ D'). Proof. use antisymm_dcpo. - use dcpo_lub_is_least. intro i. use prod_dcpo_le ; cbn in *. + use less_than_dcpo_lub. * exact (pr1 i). * apply refl_dcpo. + use less_than_dcpo_lub. * exact (pr2 i). * apply refl_dcpo. - assert (Di := directed_set_el D). revert Di. use factor_through_squash ; [ apply propproperty | ]. intro Di. assert (Di' := directed_set_el D'). revert Di'. use factor_through_squash ; [ apply propproperty | ]. intro Di'. use prod_dcpo_le. + use dcpo_lub_is_least. intro i. refine (pr1 (less_than_dcpo_lub (prod_directed_set_dcpo D D') (D i ,, D' Di') (i ,, Di') _)). use prod_dcpo_le ; cbn. * apply refl_dcpo. * apply refl_dcpo. + use dcpo_lub_is_least. intro i'. refine (pr2 (less_than_dcpo_lub (prod_directed_set_dcpo D D') (D Di ,, D' i') (Di ,, i') _)). use prod_dcpo_le ; cbn. * apply refl_dcpo. * apply refl_dcpo. 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.