tendsto_Ioc_atTop_atTop

Mathlib.Order.Filter.Interval

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

English

Similarly, there is a TendstoIxxClass instance for Ioc from atTop to atTop.

Русский

Аналогично существует экземпляр TendstoIxxClass для Ioc от atTop к atTop.

LaTeX

$$$\\text{Ioc atTop atTop}$$$

Lean4

instance tendsto_Ioc_atTop_atTop : TendstoIxxClass Ioc (atTop : Filter α) atTop :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

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

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

Разделы

Аффилиация

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