Lemma scott_continuous_map_coordinates_monotone : is_monotone (X × Y) Z f. 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.
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.