Proposition scott_continuous_map_coordinates : scott_continuous_map (X × Y) Z. Proof. refine (f ,, _). use is_scott_continuous_chosen_lub. - exact scott_continuous_map_coordinates_monotone. - intros I D HD. exact (scott_continuous_map_coordinates_lub (I ,, D ,, HD)). Defined.
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.