abs — Mathlib

English

If f is ContDiffWithinAt on s at x and f(x) ≠ 0 for that x, then |f| is ContDiffWithinAt on s at x.

Русский

Если f является ContDiffWithinAt на s в точке x и f(x) ≠ 0, то |f| также ContDiffWithinAt на s в точке x.

LaTeX

$$(hf : ContDiffWithinAt Real n f s x) ∧ (h0 : f x ≠ 0) ⇒ ContDiffWithinAt Real n ($ \lambda y, |f y| $) s x$$

Lean4

theorem abs (hf : ContDiffWithinAt ℝ n f s x) (h₀ : f x ≠ 0) : ContDiffWithinAt ℝ n (fun y ↦ |f y|) s x :=
  (contDiffAt_abs h₀).comp_contDiffWithinAt x hf

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