tendsto_Ioc_atBot_atBot

Mathlib.Order.Filter.Interval

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

English

There is a TendstoIxxClass instance for Ioc from atBot to atBot.

Русский

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

LaTeX

$$$\\text{Ioc atBot atBot}$$$

Lean4

instance tendsto_Ioc_atBot_atBot : TendstoIxxClass Ioc (atBot : Filter α) atBot :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

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

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

Разделы

Аффилиация

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