differentiableWithinAt_pow — Mathlib

English

The HasFDerivAt.pow' lemma asserts the standard derivative formula for f^n in the Fréchet sense with left/right scalar actions, globally.

Русский

Лемма HasFDerivAt.pow' утверждает стандартную формулу производной f^n в смысле Фрете с левого и правого действия, глобально.

LaTeX

$$$\\mathrm{HasFDerivAt}\\ f f' x \\Rightarrow \\mathrm{HasFDerivAt}\\ (f^n) \\ (\\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; f' \\; f(x)^i)\\ x$$$

Lean4

theorem differentiableWithinAt_pow (n : ℕ) {x : 𝔸} {s : Set 𝔸} : DifferentiableWithinAt 𝕜 (fun x : 𝔸 => x ^ n) s x :=
  differentiableWithinAt_id.pow _

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