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. 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.
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.