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