proposition: Lemma scott_continuous_map_coordinates_lub (D : directed_set (X × Y)) : F (⨆ D) = ⨆ (F {{ D }}).
proof: Proof. rewrite prod_dcpo_lub. etrans. { exact (scott_continuous_map_on_lub (Fy D) (π₁ {{ D }})). } refine (_ @ !(monotone_prod_map_fubini_pair_l _ _)). use dcpo_lub_eq_pointwise. intro i ; cbn. etrans. { exact (scott_continuous_map_on_lub (_ ,, Hf₁ i) (π₂ {{ D }})). } use dcpo_lub_eq_pointwise. intro. apply idpath. 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