differentiableOn_abs — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem differentiableOn_abs {s : Set ℝ} (hs : ∀ x ∈ s, x ≠ 0) : DifferentiableOn ℝ (|·|) s := fun x hx ↦
  differentiableWithinAt_abs s (hs x hx)

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