abs — Mathlib

English

If f is differentiable on the whole space and f(x) ≠ 0 for all x, then |f| is differentiable on the space.

Русский

Если f дифференцируема на всей пространстве и f(x) ≠ 0 для всех x, тогда |f| дифференцируема на всем пространстве.

LaTeX

$$$\text{Differentiable}\ of\ (|f|) \text{ given } (\text{Differentiable } f) \, (\forall x, f(x) \neq 0)$$$

Lean4

theorem abs (hf : Differentiable ℝ f) (h₀ : ∀ x, f x ≠ 0) : Differentiable ℝ (fun x ↦ |f x|) := fun x ↦
  (hf x).abs (h₀ x)

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