tendsto_Ioo_Iic_Iio — Mathlib

English

In a preorder α and a ∈ α, the Ioo interval yields a Tendsto relation from 𝓟(Iic a) to 𝓟(Iio a), reflecting convergence within a two-sided bounded region around a.

Русский

В предобратстве α и при a ∈ α интервал Ioo задаёт схождение от 𝓟(Iic a) к 𝓟(Iio a), отображая сходимость в двухсторонней ограниченной окрестности вокруг a.

LaTeX

$$$$ \operatorname{TendstoIxxClass}(Ioo, \mathcal{P}(\mathrm{Iic}(a)), \mathcal{P}(\mathrm{Iio}(a))) $$$$

Lean4

instance tendsto_Ioo_Iic_Iio {a : α} : TendstoIxxClass Ioo (𝓟 (Iic a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ico_self

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