Proposition is_scott_continuous_lam {X Y Z : dcpo} (f : scott_continuous_map (X × Z) Y) (H : ∏ (z : Z), is_scott_continuous (pr2 X) (pr2 Y) (λ x, f (x ,, z))) : is_scott_continuous Z (dcpo_funspace X Y) (λ z, (λ x, f(x ,, z)) ,, H z). Proof. use make_is_scott_continuous. - abstract (intros z₁ z₂ p x ; apply (is_monotone_scott_continuous_map f) ; exact (prod_dcpo_le (x ,, z₁) (x ,, z₂) (refl_dcpo _) p)). - intros D. use eq_scott_continuous_map. intro x ; cbn. etrans. { apply maponpaths. apply maponpaths_2. exact (!(const_lub x D (directed_set_el D))). } etrans. { apply maponpaths. refine (!_). apply prod_dcpo_lub'. } rewrite scott_continuous_map_on_lub. rewrite prod_dcpo_monotone_lub_const_l. unfold pointwise_lub. use antisymm_dcpo. + use dcpo_lub_is_least. cbn ; intro i. use less_than_dcpo_lub ; cbn. * exact i. * apply refl_dcpo. + use dcpo_lub_is_least. cbn ; intro i. use less_than_dcpo_lub ; cbn. * exact i. * apply refl_dcpo. Qed.
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.