English
Let α be a preordered set and a ∈ α. The interval Ioc with left-closed right-open endpoints relative to a yields a Tendsto from the principal filter on Iic a to itself, i.e., there is a stable convergence behavior within the left-bounded interval at a.
Русский
Пусть α — упорядоченное множество и a ∈ α. Интервал Ioc с левой закрытой и правой открытой границей относительно a задаёт сходимость внутри левого ограниченного интервала Iic a: существует устойчивое поведение сходимости внутри этого фильтра.
LaTeX
$$$$ \operatorname{TendstoIxxClass}(Ioc, \mathcal{P}(\mathrm{Iic}(a)), \mathcal{P}(\mathrm{Iic}(a))) $$$$
Lean4
instance tendsto_Ioc_Iic_Iic {a : α} : TendstoIxxClass Ioc (𝓟 (Iic a)) (𝓟 (Iic a)) :=
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self
