contDiffWithinAt_abs — Mathlib

English

For x ≠ 0, the absolute value map is ContDiffWithinAt at x for any set s.

Русский

Для x ≠ 0 отображение модуля |·| является ContDiffWithinAt в точке x для любого множества s.

LaTeX

$${x : Real} (hx : x ≠ 0) (s : Set Real) : ContDiffWithinAt Real n (|\cdot|) s x$$

Lean4

theorem contDiffWithinAt_abs {x : ℝ} (hx : x ≠ 0) (s : Set ℝ) : ContDiffWithinAt ℝ n (|·|) s x :=
  (contDiffAt_abs hx).contDiffWithinAt

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