Proposition scott_continuous_map_eq_on_basis {Y : dcpo} {f g : scott_continuous_map X Y} (p : ∏ (i : B), f (B i) = g (B i)) : f = g. Proof. use eq_scott_continuous_map. intro x. refine (maponpaths f (!((approximating_basis_lub B x))) @ _). refine (_ @ maponpaths g (approximating_basis_lub B x)). rewrite !scott_continuous_map_on_lub. use antisymm_dcpo. - use dcpo_lub_is_least ; cbn. intro i. use less_than_dcpo_lub ; cbn. + exact i. + unfold basis_below_map. rewrite p. apply refl_dcpo. - use dcpo_lub_is_least ; cbn. intro i. use less_than_dcpo_lub ; cbn. + exact i. + unfold basis_below_map. rewrite p. apply refl_dcpo. 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.