Proposition scott_continuous_map_from_basis_le (i : B) : scott_continuous_map_from_basis (B i) ⊑ f i. Proof. use dcpo_lub_is_least ; cbn. intro j. induction j as [ j p ] ; cbn. apply Hf. exact 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.