proposition: Lemma scott_continuous_map_coordinates_monotone : is_monotone (X × Y) Z f.
proof: Proof. intros xy₁ xy₂ pq. induction xy₁ as [ x₁ y₁ ]. induction xy₂ as [ x₂ y₂ ]. induction pq as [ p q ]. pose (is_scott_continuous_monotone (Hf₁ x₁) _ _ q) as r₁. pose (is_scott_continuous_monotone (Hf₂ y₂) _ _ p) as r₂. cbn in *. exact (trans_PartialOrder Z r₁ r₂). 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