Proposition is_strict_scott_continuous_prodtofun {W X Y : hSet} {DW : dcppo_struct W} {DX : dcppo_struct X} {DY : dcppo_struct Y} {f : W → X} (Hf : is_strict_scott_continuous DW DX f) {g : W → Y} (Hg : is_strict_scott_continuous DW DY g) : is_strict_scott_continuous DW (prod_dcppo_struct DX DY) (prodtofuntoprod (f ,, g)). Proof. split. - exact (is_scott_continuous_prodtofun Hf Hg). - use pathsdirprod. + apply Hf. + apply Hg. 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.