abs — Mathlib

English

If f has derivative f' at x within s, and f(x) ≠ 0, then the derivative of |f| at x within s is (sign(f(x)) ) times f'.

Русский

Если у f в точке x внутри s существует производная f' и f(x) ≠ 0, то производная |f| в x равна sign(f(x)) · f'.

LaTeX

$$$\operatorname{HasFDerivWithinAt} f f' s x \Rightarrow f(x) \neq 0 \Rightarrow \operatorname{HasFDerivWithinAt} (|f(x)|) ((\operatorname{SignType.sign} (f(x)) : \mathbb{R}) \cdot f') \, s \ x$$$

Lean4

theorem abs (hf : HasFDerivWithinAt f f' s x) (h₀ : f x ≠ 0) :
    HasFDerivWithinAt (fun x ↦ |f x|) ((SignType.sign (f x) : ℝ) • f') s x :=
  (hasDerivAt_abs h₀).comp_hasFDerivWithinAt x hf

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