derivWithin_zpow — Mathlib

English

For a function t ↦ t^m, the derivative within s at x equals m x^{m−1} whenever s has a differentiable structure there (UniqueDiffWithinAt).

Русский

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

LaTeX

$$$\\text{derivWithin } (t \\mapsto t^m) \\, s \\, x = m \\cdot x^{m-1}$ under appropriate differentiability conditions$$

Lean4

theorem derivWithin_zpow (hxs : UniqueDiffWithinAt 𝕜 s x) (h : x ≠ 0 ∨ 0 ≤ m) :
    derivWithin (fun x => x ^ m) s x = (m : 𝕜) * x ^ (m - 1) :=
  (hasDerivWithinAt_zpow m x h s).derivWithin hxs

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