cpow_const — Mathlib

English

Let f be differentiable within s at x and f(x) lie in the slit plane. Then the derivative of x ↦ f(x)^{c} at x (within s) is c f(x)^{c-1} f'(x).

Русский

Пусть f дифференцируема внутри s в x и f(x) лежит в slitPlane. Тогда производная x ↦ f(x)^{c} внутри s равна c f(x)^{c-1} f'(x).

LaTeX

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

Lean4

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

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