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. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. 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.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Section ScottContinuousFromBasis. End ScottContinuousFromBasis.