Definition lam_scott_continuous_map {X Y Z : dcpo} (f : scott_continuous_map (X × Z) Y) : scott_continuous_map Z (dcpo_funspace X Y). Proof. refine (_ ,, is_scott_continuous_lam f _). abstract (intro z ; refine (comp_is_scott_continuous _ (pr2 f)) ; use is_scott_continuous_prodtofun ; [ apply id_is_scott_continuous | apply is_scott_continuous_constant ]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. 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.FubiniTheorem. Require Import UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.