proposition: Proposition is_scott_continuous_dirprod_pr1 {X Y : hSet} (DX : dcpo_struct X) (DY : dcpo_struct Y) : is_scott_continuous (prod_dcpo_struct DX DY) DX dirprod_pr1.
proof: Proof. split. - apply dirprod_pr1_is_monotone. - intros I DI HD x Hx. split. + intros i. exact (pr1 (is_least_upperbound_is_upperbound Hx i)). + intros x' Hx'. refine (pr1 (is_least_upperbound_is_least Hx (x' ,, pr2 x) _)). intro i. split ; cbn. * exact (Hx' i). * exact (pr2 (is_least_upperbound_is_upperbound Hx i)). 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