tendsto_ofReal_atTop

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.tendsto_ofReal_atTop

English

The neighborhood filter at 0 has a basis given by Iio a for a>0.

Русский

Система баз окрестностей нуля задаётся интерфейсами Iio a при a>0.

LaTeX

$$$ (nhds(0)).HasBasis (\\lambda a: a>0) (\\lambda a: Iio a) $$$

Lean4

theorem tendsto_ofReal_atTop : Tendsto ENNReal.ofReal atTop (𝓝 ∞) :=
  tendsto_ofReal_nhds_top.2 tendsto_id

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

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

Разделы

Аффилиация

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