English
If f is differentiable within s at x, hx holds, and s has a unique differentiation point at x, then the derivative within s of f(x)^p equals derivWithin f s x times p times f(x)^{p−1}. That is, derivWithin (f^p) s x = derivWithin f s x · p · f(x)^{p−1}.
Русский
Если f дифференцируема внутри s в точке x, выполняются условия hx и уникальности точки, то производная внутри s от f(x)^p равна derivWithin f s x, умноженной на p и на f(x)^{p−1}. То есть derivWithin (f^p) s x = derivWithin f s x · p · f(x)^{p−1}.
LaTeX
$$$\\displaystyle \\text{derivWithin} (\\lambda x. f(x)^p)\\, s\\, x = \\text{derivWithin} f\\, s\\, x \\cdot p \\cdot f(x)^{\\,p-1}$$$
Lean4
theorem derivWithin_rpow_const (hf : DifferentiableWithinAt ℝ f s x) (hx : f x ≠ 0 ∨ 1 ≤ p)
(hxs : UniqueDiffWithinAt ℝ s x) : derivWithin (fun x => f x ^ p) s x = derivWithin f s x * p * f x ^ (p - 1) :=
(hf.hasDerivWithinAt.rpow_const hx).derivWithin hxs
