derivWithin_cexp — Mathlib

English

The exponential is differentiable at every point of the complex plane, i.e., differentiableAt exp x holds for all x.

Русский

Экспонента дифференцируема во всех точках плоскости, то есть differentiableAt exp x выполняется для всех x.

LaTeX

$$$ \\forall x \\in \\mathbb{C}, \\text{DifferentiableAt}(\\exp, x)$$$

Lean4

theorem derivWithin_cexp (hf : DifferentiableWithinAt 𝕜 f s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin (fun x => Complex.exp (f x)) s x = Complex.exp (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.cexp.derivWithin hxs

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