fun_pow — Mathlib

English

If h is HasDerivWithinAt f f' s x, then HasDerivWithinAt (f^n) (sum) s x holds for every n.

Русский

Если имеем HasDerivWithinAt f с производной f' внутри s в x, то HasDerivWithinAt (f^n) выполняется для любого n.

LaTeX

$$$$\\text{HasDerivWithinAt}(f^n,\\; \\sum_{i=0}^{n-1} f(x)^{\,n-1-i}\\, f'(x)\\, f(x)^i,\\; s,\\ x). $$$$

Lean4

nonrec theorem fun_pow (h : HasDerivWithinAt f f' s x) (n : ℕ) :
    HasDerivWithinAt (fun x ↦ f x ^ n) (n * f x ^ (n - 1) * f') s x := by
  simpa using h.hasFDerivWithinAt.pow n |>.hasDerivWithinAt

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