tendsto_Ioo_atTop_atTop

Mathlib.Order.Filter.Interval

URI: https://scilib.ai/kg/mathlib#Filter.tendsto_Ioo_atTop_atTop

English

There is a TendstoIxxClass instance for Ioo from atTop to atTop.

Русский

Существует экземпляр TendstoIxxClass для Ioo от atTop к atTop.

LaTeX

$$$\\text{Ioo atTop atTop}$$$

Lean4

instance tendsto_Ioo_atTop_atTop : TendstoIxxClass Ioo (atTop : Filter α) atTop :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

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

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

Разделы

Аффилиация

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