abs_of_pos

Mathlib.Analysis.Calculus.Deriv.Abs

URI: https://scilib.ai/kg/mathlib#HasFDerivAt.abs_of_pos

← MathLib Explorer

English

If f(x) ≠ 0, then abs f has a derivative equal to (sign f(x)) • f'.

Русский

Если f(x) ≠ 0, то d|f| = sign(f(x))·df в x.

LaTeX

$$HasStrictFDerivAt f f' x ∧ f x ≠ 0 ⇒ HasStrictFDerivAt ($ \lambda x, |f x| $) (SignType.sign (f x) • f') x$$

Lean4

theorem abs_of_pos (hf : HasFDerivAt f f' x) (h₀ : 0 < f x) : HasFDerivAt (fun x ↦ |f x|) f' x :=
  by
  convert (hasDerivAt_abs_pos h₀).hasFDerivAt.comp x hf using 1
  ext y
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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