differentiableAt_abs_neg — Mathlib

English

A real-valued abs function is differentiable at any negative point.

Русский

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

LaTeX

$$$\text{differentiableAt}_{\mathbb{R}} (|\cdot|) x \quad \text{ если } x < 0$$$

Lean4

theorem differentiableAt_abs_neg {x : ℝ} (hx : x < 0) : DifferentiableAt ℝ (|·|) x :=
  (hasDerivAt_abs_neg hx).differentiableAt

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