proposition: Proposition is_scott_continuous_prodtofun {W X Y : hSet} {DW : dcpo_struct W} {DX : dcpo_struct X} {DY : dcpo_struct Y} {f : W → X} (Hf : is_scott_continuous DW DX f) {g : W → Y} (Hg : is_scott_continuous DW DY g) : is_scott_continuous DW (prod_dcpo_struct DX DY) (prodtofuntoprod (f ,, g)).
proof: Proof. split. - apply prodtofun_is_monotone. + exact (is_scott_continuous_monotone Hf). + exact (is_scott_continuous_monotone Hg). - intros I D HD w Hw. split. + intro i. split ; cbn. * exact (is_least_upperbound_is_upperbound (is_scott_continuous_lub Hf HD w Hw) i). * exact (is_least_upperbound_is_upperbound (is_scott_continuous_lub Hg HD w Hw) i). + intros xy Hxy. split ; cbn. * use (is_least_upperbound_is_least (is_scott_continuous_lub Hf HD w Hw) (pr1 xy)). intro i. exact (pr1 (Hxy i)). * use (is_least_upperbound_is_least (is_scott_continuous_lub Hg HD w Hw) (pr2 xy)). intro i. exact (pr2 (Hxy 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