hasFDerivWithinAt_pow — Mathlib

English

Within a set, the derivative of f^n is the same sum as above, under the assumption of differentiability within.

Русский

Внутри множества производная f^n совпадает с суммой вышепри условии дифференцируемости внутри.

LaTeX

$$$fderivWithin_{\\mathbb{K}}(f^n)(s,x) = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; fderivWithin_{\\mathbb{K}}f(s,x) \\; f(x)^i.$$$

Lean4

theorem hasFDerivWithinAt_pow (n : ℕ) {x : 𝔸} {s : Set 𝔸} :
    HasFDerivWithinAt (𝕜 := 𝕜) (fun x : 𝔸 ↦ x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) s x :=
  hasFDerivWithinAt_id _ _ |>.pow n

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