hasDerivAt_abs_pos

Mathlib.Analysis.Calculus.Deriv.Abs

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

English

If x > 0, then HasDerivAt (|·|) 1 x.

Русский

Если x > 0, то производная abs в x равна 1.

LaTeX

$${x ∈ ℝ, x > 0} ⇒ HasDerivAt (|·|) 1 x$$

Lean4

theorem hasDerivAt_abs_pos {x : ℝ} (hx : 0 < x) : HasDerivAt (|·|) 1 x :=
  (hasStrictDerivAt_abs_pos hx).hasDerivAt

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

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

Разделы

Аффилиация

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