differentiableAt_abs_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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