proposition: Proposition map_le_on_basis_if_scott_continuous {Y : dcpo} {f g : X → Y} (p : ∏ (i : B), f (B i) ⊑ g (B i)) (Hf : is_scott_continuous X Y f) (Hg : is_scott_continuous X Y g) (x : X) : f x ⊑ g x.
proof: Proof. exact (@scott_continuous_map_le_on_basis Y (f ,, Hf) (g ,, Hg) p x). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous