Proposition monotone_prod_map_fubini_pair_l {X Y Z : dcpo} (f : monotone_function (X × Y) Z) (D : directed_set (X × Y)) : ⨆_{D} f = ⨆_{π₁ {{D}}} fubini_monotone_function_l f D. Proof. use (eq_lub Z (f {{ D }})). - apply is_least_upperbound_dcpo_comp_lub. - use make_dcpo_is_least_upperbound. + cbn ; intro i. use less_than_dcpo_lub. * exact i. * cbn. use less_than_dcpo_lub. ** exact i. ** apply refl_PartialOrder. + intros x' Hx'. use dcpo_lub_is_least ; cbn ; cbn in Hx'. intro i. use dcpo_lub_is_least ; cbn. intro j. assert (H := is_directed_top (directed_set_is_directed D) i j). revert H. use factor_through_squash. { apply propproperty. } intros kH. induction kH as [ k [ H₁ H₂ ]]. refine (trans_PartialOrder Z _ (Hx' k)). apply f. split. * exact (pr1 H₁). * exact (pr2 H₂). 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.Examples.BinaryProducts.