fact: Definition fubini_monotone_function_l {X Y Z : dcpo} (f : monotone_function (X × Y) Z) (D : directed_set (X × Y)) : monotone_function X Z.
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.Examples.BinaryProducts