proposition: 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: 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.
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