exp — Mathlib

English

If f tends to a, then exp( f ) tends to exp(a).

Русский

Если функция сходится к пределу a, то экспонента цепной функции сходится к exp(a).

LaTeX

$$$\operatorname{Tendsto} \big( f \big) \; \Rightarrow \; \operatorname{Tendsto} \big( x \mapsto \exp 𝕂 (f x) \big) \; (l) \; \operatorname{nhds}(\exp 𝕂 a)$$$

Lean4

theorem _root_.Filter.Tendsto.exp {α : Type*} {l : Filter α} {f : α → 𝔸} {a : 𝔸} (hf : Tendsto f l (𝓝 a)) :
    Tendsto (fun x => exp 𝕂 (f x)) l (𝓝 (exp 𝕂 a)) :=
  (exp_continuous.tendsto _).comp hf

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