proposition: Lemma Cmap_wd_loc : forall (X Y : MetricSpace) (plX : PrelengthSpace X) (f g : X --> Y) (x : Complete X) (e : Qpos), (forall a : X, ball (proj1_sig e) (Cunit a) x -> msp_eq (f a) (g a)) -> msp_eq (Cmap_fun plX f x) (Cmap_fun plX g x).
proof: Proof. intros. rewrite Cmap_fun_correct. rewrite Cmap_fun_correct. apply Cmap_slow_wd_loc with (e:=e). exact H. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q