cexp — Mathlib

English

If f is analytic on a neighborhood of a subset s, then exp(f) is analytic on that same neighborhood.

Русский

Если f аналитична на окрестности множества s, то e^{f} аналитична на той же окрестности.

LaTeX

$$$ \\operatorname{AnalyticOnNhd}_{\\mathbb{C}}(f;s) \\Rightarrow \\operatorname{AnalyticOnNhd}_{\\mathbb{C}}(\\exp \\circ f;s)$$$

Lean4

/-- `exp ∘ f` is analytic -/
theorem «cexp» (fs : AnalyticOnNhd ℂ f s) : AnalyticOnNhd ℂ (fun z ↦ exp (f z)) s := fun z n ↦
  analyticAt_cexp.comp (fs z n)

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