tendsto_Icc_atTop_atTop — Mathlib

English

There is a TendstoIxxClass instance for Icc from atTop to atTop: the interval operation Icc is preserved at infinity.

Русский

Существует экземпляр TendstoIxxClass для Icc от фильтра atTop к atTop: операция интервала сохраняется при движении к бесконечности.

LaTeX

$$$\\text{TendstoIxxClass } Icc (\\text{atTop}) (\\text{atTop})$$$

Lean4

instance tendsto_Icc_atTop_atTop : TendstoIxxClass Icc (atTop : Filter α) atTop :=
  (hasBasis_iInf_principal_finite _).tendstoIxxClass fun _ _ =>
    Set.OrdConnected.out <| ordConnected_biInter fun _ _ => ordConnected_Ici

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