English
If f is differentiable within s at x, g is differentiable within s at x, and f(x) ≠ g(x), then y ↦ dist(f(y), g(y)) is differentiable within s at x.
Русский
Если f и g дифференцируемы внутри s в x и f(x) ≠ g(x), то y ↦ dist(f(y), g(y)) дифференцируема внутри s в x.
LaTeX
$$$\text{DifferentiableWithinAt}_{\mathbb{R}}(f,s,x) \land \text{DifferentiableWithinAt}_{\mathbb{R}}(g,s,x) \land f(x) \neq g(x) \Rightarrow \text{DifferentiableWithinAt}_{\mathbb{R}}(y \mapsto \operatorname{dist}(f(y), g(y)), s, x).$$$
Lean4
theorem dist (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) (hne : f x ≠ g x) :
DifferentiableWithinAt ℝ (fun y => dist (f y) (g y)) s x :=
by
simp only [dist_eq_norm]
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)
