proposition: 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: Proof. exact (pr2 (@scott_continuous_map_coordinates (X ,, DX) (Y ,, DY) (Z ,, DZ) f Hf₁ Hf₂)). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.FubiniTheorem UniMath.OrderTheory.DCPOs.Examples.BinaryProducts