deriv_abs — Mathlib

English

The derivative of |x| is sign(x); in particular, it equals 0 at x=0 and equals sign(x) for x ≠ 0.

Русский

Производная |x| равна sign(x); в частности, при x ≠ 0 равна sign(x), а в точке x=0 равна 0.

LaTeX

$$$\displaystyle \frac{d}{dx}|x| = \begin{cases} \operatorname{sign}(x), & x \neq 0, \\ 0, & x = 0. \end{cases}$$$

Lean4

theorem deriv_abs (x : ℝ) : deriv (|·|) x = SignType.sign x :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · simpa using deriv_abs_zero
  · simpa [hx] using (hasDerivAt_abs hx).deriv

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