dist — Mathlib

English

If f and g are ContDiffOn on s and f x ≠ g x for all x ∈ s, then y ↦ dist(f(y), g(y)) is ContDiffOn on s.

Русский

Если f и g — ContDiffOn на s и для всех x ∈ s выполняется f(x) ≠ g(x), то y ↦ dist(f(y), g(y)) дифференцируема внутри s.

LaTeX

$$$$\text{ContDiffOn}_{\mathbb{R}}^n f\,s \Rightarrow \text{ContDiffOn}_{\mathbb{R}}^n g\,s \Rightarrow (\forall x\in s, f(x) \neq g(x)) \Rightarrow \text{ContDiffOn}_{\mathbb{R}}^n (\,y \mapsto \operatorname{dist}(f(y), g(y))\,) s.$$$$

Lean4

theorem dist (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (hne : f x ≠ g x) :
    DifferentiableAt ℝ (fun y => dist (f y) (g y)) x := by simp only [dist_eq_norm];
  exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Похожие утверждения