Proposition is_scott_continuous_coordinates {X Y Z : hSet} (DX : dcpo_struct X) (DY : dcpo_struct Y) (DZ : dcpo_struct Z) (f : X × Y → Z) (Hf₁ : ∏ (x : X), is_scott_continuous DY DZ (λ y, f (x ,, y))) (Hf₂ : ∏ (y : Y), is_scott_continuous DX DZ (λ x, f (x ,, y))) : is_scott_continuous (prod_dcpo_struct DX DY) DZ f. Proof. exact (pr2 (@scott_continuous_map_coordinates (X ,, DX) (Y ,, DY) (Z ,, DZ) f Hf₁ Hf₂)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. 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.FubiniTheorem. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.