proposition: Lemma differentiable_pt_lim_ext : forall f1 f2 x y lx ly, locally_2d (fun u v => f1 u v = f2 u v) x y -> differentiable_pt_lim f1 x y lx ly -> differentiable_pt_lim f2 x y lx ly.
proof: Proof. intros f1 f2 x y lx ly H H1 eps. apply: locally_2d_impl (H1 eps) => {H1}. rewrite (locally_2d_singleton _ _ _ H). apply: locally_2d_impl H. apply locally_2d_forall. now intros u v ->. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive