proposition: Proposition scott_continuous_map_le_on_basis {Y : dcpo} {f g : scott_continuous_map X Y} (p : ∏ (i : B), f (B i) ⊑ g (B i)) (x : X) : f x ⊑ g x.
proof: Proof. rewrite (maponpaths f (!((approximating_basis_lub B x)))). rewrite (maponpaths g (!(approximating_basis_lub B x))). rewrite !scott_continuous_map_on_lub. use dcpo_lub_is_least ; cbn. intro i. use less_than_dcpo_lub ; cbn. - exact i. - unfold basis_below_map. apply p. 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