hasDerivWithinAt_zpow — Mathlib

English

For any m, x and any set s, if x ≠ 0 or m ≥ 0, then HasDerivWithinAt (t ↦ t^m) at x with any set s has the same derivative formula m x^{m−1}.

Русский

Для любого m, x и любого множества s, при условии x ≠ 0 или m ≥ 0, производная внутри множества s функции t^m в точке x равна m x^{m−1}.

LaTeX

$$$m:\\\\mathbb{Z}, x:\\\\mathbb{K}, h:(x \\neq 0 \\\\lor \\\\ 0 \\le m), s: Set\\\\ 𝕜 \\Rightarrow HasDerivWithinAt (\\\\lambda t, t^m) s x = ((m \\\\text{(as 𝕜)}) \\\\cdot x^{m-1})$$$

Lean4

theorem hasDerivWithinAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) (s : Set 𝕜) :
    HasDerivWithinAt (fun x => x ^ m) ((m : 𝕜) * x ^ (m - 1)) s x :=
  (hasDerivAt_zpow m x h).hasDerivWithinAt

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