abs — Mathlib

English

If f is differentiable on s and f(x) ≠ 0 for all x ∈ s, then abs f is differentiable on s.

Русский

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

LaTeX

$$$\text{DifferentiableOn}\ (\lambda x, f(x))\ s \Rightarrow \forall x\in s, f(x) \neq 0 \Rightarrow \text{DifferentiableOn}\ (|f|)\ s$$$

Lean4

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

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