English
If f tends to z in a filter l, then exp(f) tends to exp(z) in 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 «rexp» {l : Filter α} {f : α → ℝ} {z : ℝ} (hf : Tendsto f l (𝓝 z)) :
Tendsto (fun x => exp (f x)) l (𝓝 (exp z)) :=
(continuous_exp.tendsto _).comp hf