contDiffAt_abs — Mathlib

English

At any x ≠ 0, the map t ↦ |t| is ContDiffOfOrder n at x; i.e., |t| is n-times continuously differentiable at every nonzero point.

Русский

Для каждого x ≠ 0 функция t ↦ |t| является N-раз непрерывно дифференцируемой в точке x.

LaTeX

$$$x \neq 0 \Rightarrow \text{ContDiffAt}_{\mathbb{R}}(n)(|\cdot|)(x)$$$

Lean4

theorem contDiffAt_abs {x : ℝ} (hx : x ≠ 0) : ContDiffAt ℝ n (|·|) x :=
  contDiffAt_norm ℝ hx

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