deriv_abs_pos

Mathlib.Analysis.Calculus.Deriv.Abs

URI: https://scilib.ai/kg/mathlib#deriv_abs_pos

English

The derivative of |x| at a positive x is 1.

Русский

Производная |x| в точке x>0 равна 1.

LaTeX

$$$\frac{d}{dx}|x|\Big|_{x>0} = 1$$$

Lean4

theorem deriv_abs_pos {x : ℝ} (hx : 0 < x) : deriv (|·|) x = 1 :=
  (hasDerivAt_abs_pos hx).deriv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru