tendsto_Ioo_atBot_atBot

Mathlib.Order.Filter.Interval

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

English

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

Русский

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

LaTeX

$$$\\text{Ioo atBot atBot}$$$

Lean4

instance tendsto_Ioo_atBot_atBot : TendstoIxxClass Ioo (atBot : Filter α) atBot :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

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

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

Разделы

Аффилиация

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