rexp — Mathlib

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

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