contDiffOn_abs — Mathlib

English

If f is ContDiffOn on s whenever x ∈ s and f x ≠ 0 for all x ∈ s, then the composition x ↦ |f(x)| is ContDiffOn on s.

Русский

Если f является ContDiffOn на s и для всех x ∈ s имеет место f(x) ≠ 0, то x ↦ |f(x)| является ContDiffOn на s.

LaTeX

$$ContDiffOn Real n (|\cdot|) s ↔ (∀ x ∈ s, x ≠ 0) → ContDiffOn Real n f s$$

Lean4

theorem contDiffOn_abs {s : Set ℝ} (hs : ∀ x ∈ s, x ≠ 0) : ContDiffOn ℝ n (|·|) s := fun x hx ↦
  contDiffWithinAt_abs (hs x hx) s

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