cexp — Mathlib

English

If f is analytic within a set s at a point x, then the function z ↦ exp(f(z)) is analytic within the same set at x.

Русский

Если f аналитична внутри множества s в точке x, то функция z ↦ e^{f(z)} аналитична внутри того же множества в x.

LaTeX

$$$ \\operatorname{AnalyticWithinAt}_{\\mathbb{C}}(f;s;x) \\Longrightarrow \\operatorname{AnalyticWithinAt}_{\\mathbb{C}}(\\exp \\circ f;s;x)$$$

Lean4

theorem «cexp» (fa : AnalyticWithinAt ℂ f s x) : AnalyticWithinAt ℂ (fun z ↦ exp (f z)) s x :=
  analyticAt_cexp.comp_analyticWithinAt fa

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