abs_of_pos — Mathlib

English

If f is differentiable within s at x and f(x) < 0, then |f| is differentiable within s at x.

Русский

Если f дифференцируема внутри s в x и f(x) < 0, то |f| дифференцируема внутри s в x.

LaTeX

$$$\text{differentiableWithinAt}_{\mathbb{R}} (|f|) \ s \ x \quad \text{ если } f(x) < 0$$$

Lean4

theorem abs_of_pos (hf : DifferentiableWithinAt ℝ f s x) (h₀ : 0 < f x) :
    DifferentiableWithinAt ℝ (fun x ↦ |f x|) s x :=
  (differentiableAt_abs_pos h₀).comp_differentiableWithinAt x hf

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