tendsto_Icc_Icc_Icc — Mathlib

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

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