abs_of_neg — Mathlib

English

Let f be differentiable within a set s at x with derivative f'. If f(x) < 0, then the derivative of |f| at x within s is -f'.

Русский

Пусть f дифференцируема внутри множества s в точке x с производной f'. Если f(x) < 0, то производная функции |f| в точке x внутри s равна -f'.

LaTeX

$$$\operatorname{HasFDerivWithinAt} f f' s x \Rightarrow f(x) < 0 \Rightarrow \operatorname{HasFDerivWithinAt} (\lambda y, |f(y)|) (-f') \, s \ x$$$

Lean4

theorem abs_of_neg (hf : HasFDerivWithinAt f f' s x) (h₀ : f x < 0) : HasFDerivWithinAt (fun x ↦ |f x|) (-f') s x :=
  by
  convert (hasDerivAt_abs_neg h₀).comp_hasFDerivWithinAt x hf using 1
  simp

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