contDiffAt_norm — Mathlib

English

At any nonzero point x of a vector, the norm function is ContDiffAt: the map y ↦ ‖y‖ is differentiable at y = x.

Русский

В любой ненулевой точке вектора функция нормы является ContDiffAt: отображение y ↦ ‖y‖ дифференцируемо в точке y = x.

LaTeX

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

Lean4

theorem contDiffAt_norm {x : E} (hx : x ≠ 0) : ContDiffAt ℝ n norm x :=
  by
  have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
  simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this

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