English
Let α be a preordered set and a ∈ α. Then the interval operator Ioc induces a convergence-type relation from the principal filter on Ici a to the principal filter on Ioi a; in particular, this yields a Tendsto-type structure between these interval-generated filters.
Русский
Пусть α — упорядоченное множество и фиксировано a ∈ α. Тогда операция интервалов Ioc порождает отношение схождения между правой и левой границами, переводя первичный фильтр на Ici a в первичный фильтр на Ioi a; в частности существует структура типа Tendsto между соответствующими фильтрами.
LaTeX
$$$$ \operatorname{TendstoIxxClass}(Ioc, \mathcal{P}(\mathrm{Ici}(a)), \mathcal{P}(\mathrm{Ioi}(a))) $$$$
Lean4
instance tendsto_Ioc_Ici_Ioi {a : α} : TendstoIxxClass Ioc (𝓟 (Ici a)) (𝓟 (Ioi a)) :=
tendstoIxxClass_principal.2 fun _ h₁ _ _ _ h₂ => lt_of_le_of_lt h₁ h₂.1
