cexp — Mathlib

English

If a function f is ContDiffOn 𝕜 n on s, then the composition x ↦ exp(f(x)) is ContDiffOn 𝕜 n on s.

Русский

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

LaTeX

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

Lean4

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

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