cexp — Mathlib

English

If a function f(x) tends to z along a filter l, then exp(f(x)) tends to exp(z) along l.

Русский

Если функция f(x) стремится к z вдоль фильтра l, то exp(f(x)) стремится к exp(z) вдоль l.

LaTeX

$$$$ \\operatorname{Tendsto}(f, l, \\mathcal{N}(z)) \\Rightarrow \\operatorname{Tendsto}(\\exp \\circ f, l, \\mathcal{N}(\\exp z)). $$$$

Lean4

theorem «cexp» {l : Filter α} {f : α → ℂ} {z : ℂ} (hf : Tendsto f l (𝓝 z)) :
    Tendsto (fun x => exp (f x)) l (𝓝 (exp z)) :=
  (continuous_exp.tendsto _).comp hf

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