English
Let α be a preorder and a,b ∈ α. The closed interval Icc(a,b) is preserved under a Tendsto structure, giving a TendstoIxxClass from 𝓟(Icc a b) to itself.
Русский
Пусть α — предобратство и a,b ∈ α. Закрытый интервал Icc(a,b) сохраняется в рамках структуры схождения, образуя TendstoIxxClass от 𝓟(Icc a b) к самому себе.
LaTeX
$$$$ \operatorname{TendstoIxxClass}(Icc, \mathcal{P}(\mathrm{Icc}(a,b)), \mathcal{P}(\mathrm{Icc}(a,b))) $$$$
Lean4
instance tendsto_Icc_Icc_Icc {a b : α} : TendstoIxxClass Icc (𝓟 (Icc a b)) (𝓟 (Icc a b)) :=
tendstoIxxClass_principal.mpr fun _x hx _y hy => Icc_subset_Icc hx.1 hy.2