differentiableWithinAt_zpow — Mathlib

English

If x ≠ 0 or m ≥ 0, then f(x) = x^m is differentiable within any set s at x.

Русский

Если x ≠ 0 или m ≥ 0, то f(x) = x^m дифференцируема внутри любого множества s в точке x.

LaTeX

$$$x \\neq 0 \\lor 0 \\le m \\Rightarrow \\text{DifferentiableWithinAt } 𝕜 (\\lambda x, x^m) s x$$$

Lean4

theorem differentiableWithinAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
    DifferentiableWithinAt 𝕜 (fun x => x ^ m) s x :=
  (differentiableAt_zpow.mpr h).differentiableWithinAt

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