differentiableAt_zpow — Mathlib

English

The map x ↦ x^m is differentiable at x exactly when x ≠ 0 or m ≥ 0.

Русский

Отображение x ↦ x^m дифференцируемо в точке x тогда и только тогда, когда x ≠ 0 или m ≥ 0.

LaTeX

$$$\\text{DifferentiableAt } 𝕜 (\\lambda x, x^m) x \\iff x \\neq 0 \\lor 0 \\le m$$$

Lean4

theorem differentiableAt_zpow : DifferentiableAt 𝕜 (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m :=
  ⟨fun H => NormedField.continuousAt_zpow.1 H.continuousAt, fun H => (hasDerivAt_zpow m x H).differentiableAt⟩

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