tendsto_Ico_atBot_atBot

Mathlib.Order.Filter.Interval

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

English

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

Русский

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

LaTeX

$$$\\text{Ico atBot atBot}$$$

Lean4

instance tendsto_Ico_atBot_atBot : TendstoIxxClass Ico (atBot : Filter α) atBot :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

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

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

Разделы

Аффилиация

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