differentiableAt_abs — Mathlib

English

The absolute value function is differentiable at every nonzero real number.

Русский

Функция абсолютного значения дифференцируема во всех ненулевых вещественных точках.

LaTeX

$$$\text{differentiableAt}_{\mathbb{R}} |\cdot| x \quad \text{ при } x \neq 0$$$

Lean4

theorem differentiableAt_abs {x : ℝ} (hx : x ≠ 0) : DifferentiableAt ℝ (|·|) x :=
  (hasDerivAt_abs hx).differentiableAt

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