tendsto_exp_nhds_zero_nhds_one

Mathlib.Analysis.SpecialFunctions.Exp

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

← MathLib Explorer

English

exp tends to 0 as x → -∞ (equivalently, exp(−x) tends to 0 as x → +∞).

Русский

exp стремится к 0 при x → -∞ (или эквивалентно exp(−x) → 0 при x → +∞).

LaTeX

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

Lean4

/-- The real exponential function tends to `1` at `0`. -/
theorem tendsto_exp_nhds_zero_nhds_one : Tendsto exp (𝓝 0) (𝓝 1) :=
  by
  convert continuous_exp.tendsto 0
  simp

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

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

Разделы

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

Аффилиация

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