cpow_const — Mathlib

English

Let f be differentiable within s at x and f(x) ∈ slitPlane. Then within s, the derivative of x ↦ f(x)^{c} is c f(x)^{c-1} f'(x).

Русский

Пусть f дифференцируема внутри s в x и f(x) ∈ slitPlane. Тогда внутри s производная x ↦ f(x)^{c} равна 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)\\text{ (within }s).$$$

Lean4

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

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