abs — Mathlib

English

If hf is ContDiffOn on s and h0 holds for all x ∈ s (f x ≠ 0), then |f| is ContDiffOn on s.

Русский

Если hf является ContDiffOn на s и для всех x ∈ s выполняется f(x) ≠ 0, то |f| также ContDiffOn на s.

LaTeX

$$(hf : ContDiffOn Real n f s) ∧ (∀ x ∈ s, f x ≠ 0) ⇒ ContDiffOn Real n ($ \lambda y, |f y| $) s$$

Lean4

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

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