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