tendsto_exp_nhds_zero_nhds_one

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

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

English

As the argument tends to 0, exp tends to 1.

Русский

При стремлении аргумента к 0 экспентональные стремится к 1.

LaTeX

$$Tendsto \\exp (nhds 0) (nhds 1)$$

Lean4

theorem _root_.EReal.tendsto_exp_nhds_zero_nhds_one : Filter.Tendsto exp (𝓝 0) (𝓝 1) :=
  by
  convert continuous_exp.tendsto 0
  simp

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

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

Разделы

Аффилиация

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