tendsto_exp_neg_atTop_nhds_zero

Mathlib.Analysis.SpecialFunctions.Exp

URI: https://scilib.ai/kg/mathlib#Real.tendsto_exp_neg_atTop_nhds_zero

← MathLib Explorer

English

exp(-x) → 0 as x → +∞.

Русский

exp(-x) → 0 при x → +∞.

LaTeX

$$$$ \\lim_{x \\to +\\infty} \\exp(-x) = 0. $$$$

Lean4

/-- The real exponential function tends to `0` at `-∞` or, equivalently, `exp(-x)` tends to `0`
at `+∞` -/
theorem tendsto_exp_neg_atTop_nhds_zero : Tendsto (fun x => exp (-x)) atTop (𝓝 0) :=
  (tendsto_inv_atTop_zero.comp tendsto_exp_atTop).congr fun x => (exp_neg x).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru