Proposition map_eq_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. exact (maponpaths (λ z, pr1 z x) (@scott_continuous_map_eq_on_basis Y (f ,, Hf) (g ,, Hg) 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.