tendsto_exp_atBot_nhdsGT — Mathlib

English

Let l be a filter on a set and f a function to the real numbers. Then exp(f(x)) tends to 0 as x tends to −∞ (i.e., exp x vanishes at −∞).

Русский

Пусть l — фильтр на некотором множестве и f: X → ℝ. Тогда exp(f(x)) стремится к 0 при x → −∞ (то есть экспонента стремится к нулю на −∞).

LaTeX

$$$\\displaystyle \\lim_{x \\to -\\infty} e^{x} = 0.$$$

Lean4

theorem tendsto_exp_atBot_nhdsGT : Tendsto exp atBot (𝓝[>] 0) :=
  tendsto_inf.2 ⟨tendsto_exp_atBot, tendsto_principal.2 <| Eventually.of_forall exp_pos⟩

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