English
Let f: R → R be differentiable within a set s at x with derivative f'. If f(x) ≠ 0 or p ≥ 1, then the derivative within s of the function y ↦ f(y)^p at x is f'(x) · p · f(x)^{p−1}. More explicitly, d/dy [f(y)^p] (within s) at x equals f'(x) p f(x)^{p−1}.
Русский
Пусть f: ℝ → ℝ дифференцируема внутри множествa s в точке x с производной f'. Если f(x) ≠ 0 или p ≥ 1, то производная внутри s функции y ↦ f(y)^p в точке x равна f'(x) · p · f(x)^{p−1}. Более точно: производная по y внутри s от f(y)^p в точке x равна f'(x) p f(x)^{p−1}.
LaTeX
$$$\\displaystyle \\text{derivWithin} (\\lambda y. f(y)^p)\\, s\\, x = \\text{derivWithin} f\\, s\\, x \\cdot p \\cdot f(x)^{\,p-1}$$$
Lean4
theorem rpow_const (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x :=
by
convert (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1
ring
