derivWithin_pow_field — Mathlib

English

For UniqueDiffWithinAt 𝕜 s x, the derivative of x^n within s is n x^{n-1}.

Русский

При условии уникальности внутри множества производная x^n внутри s равна n x^{n-1}.

LaTeX

$$$derivWithin (fun x => x^n)\\ s\\ x = n \\cdot x^{n-1}$$$

Lean4

theorem derivWithin_pow_field (h : UniqueDiffWithinAt 𝕜 s x) (n : ℕ) :
    derivWithin (fun x => x ^ n) s x = (n : 𝕜) * x ^ (n - 1) := by
  rw [derivWithin_fun_pow (differentiableWithinAt_id' (s := s)) n, derivWithin_id' _ _ h, mul_one]

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