cexp — Mathlib

English

If f is ContDiffWithinAt 𝕜 n f s x, then x ↦ exp(f(x)) is ContDiffWithinAt 𝕜 n f s x.

Русский

Если f имеет континуированную дифференцируемость порядка n внутри области s в точке x, то exp(f(x)) имеет ту же гладкость внутри s в x.

LaTeX

$$$ \operatorname{ContDiffWithinAt}_{\mathbb{K}} n f s x \Rightarrow \operatorname{ContDiffWithinAt}_{\mathbb{K}} n \bigl( x \mapsto \mathrm{Complex.exp}(f(x)) \bigr) s x$$$

Lean4

@[fun_prop]
theorem cexp {n} (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (fun x => Complex.exp (f x)) s x :=
  Complex.contDiff_exp.contDiffAt.comp_contDiffWithinAt x hf

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