cpow_const — Mathlib

English

If f is differentiable and f(x) ∈ slitPlane, then the derivative of x ↦ f(x)^{c} is c f(x)^{c-1} f'(x).

Русский

Если f дифференцируема и f(x) ∈ slitPlane, то производная x ↦ f(x)^{c} равна c f(x)^{c-1} f'(x).

LaTeX

$$$\\text{If }f\\text{ is differentiable and }f(x)\\in\\mathrm{slitPlane},\\ \\frac{d}{dx} f(x)^{c}= c\\,f(x)^{c-1} f'(x).$$$

Lean4

theorem cpow_const (hf : HasStrictDerivAt f f' x) (h0 : f x ∈ slitPlane) :
    HasStrictDerivAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') x :=
  (Complex.hasStrictDerivAt_cpow_const h0).comp x hf

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