tendsto_Icc_atBot_atBot

Mathlib.Order.Filter.Interval

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\\text{Icc atBot atBot}$$$

Lean4

instance tendsto_Icc_atBot_atBot : TendstoIxxClass Icc (atBot : Filter α) atBot :=
  (hasBasis_iInf_principal_finite _).tendstoIxxClass fun _ _ =>
    Set.OrdConnected.out <| ordConnected_biInter fun _ _ => ordConnected_Iic

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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