pow — Mathlib

English

Within a set s, if f is differentiable up to x, then the derivative of f^n within s obeys the standard power rule with deriv f s x in place of f'.

Русский

На множестве s, если f дифференцируема в x, то производная f^n внутри s удовлетворяет обычному правилу степеней, заменив производную на deriv f s x.

LaTeX

$$$$\\operatorname{derivWithin}(f(x)^n)\\, s\\ x = \\sum_{i=0}^{n-1} f(x)^{\,n-1-i}\\, (\\operatorname{derivWithin} f\\, s\\ x)\\, f(x)^{\,i}. $$$$

Lean4

nonrec theorem pow (h : HasDerivWithinAt f f' s x) (n : ℕ) : HasDerivWithinAt (f ^ n) (n * f x ^ (n - 1) * f') s x :=
  h.fun_pow n

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