English
If f and g are ContDiffAt or ContDiff and f x ≠ g x, then the map y ↦ dist(f(y), g(y)) is ContDiffAt/ContDiff accordingly.
Русский
Если f и g дифференцируемы и расстояние между f(x) и g(x) ненулево, то отображение y ↦ dist(f(y), g(y)) дифференцируемо в соответствующем классе.
LaTeX
$$$$\text{ContDiff}_{\mathbb{R}}^n f \land \text{ContDiff}_{\mathbb{R}}^n g \land \forall x, f(x) \neq g(x) \Rightarrow \text{ContDiff}_{\mathbb{R}}^n \big( y \mapsto \operatorname{dist}(f(y), g(y))\big).$$$$
Lean4
theorem dist (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (hne : f x ≠ g x) :
ContDiffAt ℝ n (fun y => dist (f y) (g y)) x :=
by
simp only [dist_eq_norm]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
