English
Let f and g be C^n maps between normed spaces, and assume f(x) ≠ g(x) for all x. Then the distance function x ↦ dist(f(x), g(x)) is C^n.
Русский
Пусть f и g — отображения класса C^n между нормированными пространствами и для всех x выполняется f(x) ≠ g(x). Тогда функция x ↦ dist(f(x), g(x)) принадлежит классу C^n.
LaTeX
$$$ \forall f,g: \ ContDiff\_R^n f \ \land \ ContDiff\_R^n g \ \land \forall x:\ f(x) \neq g(x) \Rightarrow \ ContDiff\_R^n \big( x \mapsto \mathrm{dist}(f(x), g(x)) \big) $$$
Lean4
theorem euclidean_dist (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (h : ∀ x, f x ≠ g x) :
ContDiff ℝ n fun x => Euclidean.dist (f x) (g x) :=
by
simp only [Euclidean.dist]
apply ContDiff.dist ℝ
exacts [(toEuclidean (E := G)).contDiff.comp hf, (toEuclidean (E := G)).contDiff.comp hg, fun x =>
toEuclidean.injective.ne (h x)]
