dist — Mathlib

English

For a vector x ≠ 0, the map y ↦ ‖y‖ is ContDiffAt at y = x.

Русский

Для ненулевого вектора x отображение y ↦ ‖y‖ дифференцируемо в точке y = x.

LaTeX

$$$$\forall x \neq 0,\quad \text{ContDiffAt}_{\mathbb{R}}^n (\|\cdot\|) x.$$$$

Lean4

theorem dist (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) (hne : ∀ x, f x ≠ g x) :
    ContDiff ℝ n fun y => dist (f y) (g y) :=
  contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.dist 𝕜 hg.contDiffAt (hne x)

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