English
Let f : E → R be a function with differentiable within a set s and a fixed exponent p. If f(x) ≠ 0 or p ≥ 1, then f(x)^p is differentiable within s with derivative (p f(x)^{p-1}) times the derivative of f.
Русский
Пусть f : E → R имеет производную внутри множества s, и фиксированная степень p. Если для точки x в области определения выполняется f(x) ≠ 0 или p ≥ 1, то f(x)^p имеет внутри m производную, равную (p f(x)^{p-1}) умноженному на производную f.
LaTeX
$$$ \forall hf\,\, (h : f(x) \neq 0 \lor 1 \le p) \Rightarrow \text{HasFDerivWithinAt} (f^p) \Big( (p \cdot f(x)^{p-1}) \cdot f' \Big) s x $$$
Lean4
@[fun_prop]
theorem rpow_const (hf : HasFDerivWithinAt f f' s x) (h : f x ≠ 0 ∨ 1 ≤ p) :
HasFDerivWithinAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') s x :=
(hasDerivAt_rpow_const h).comp_hasFDerivWithinAt x hf
