tendsto_Ioo_Iio_Iio — Mathlib

English

Let α be a preorder and a ∈ α. The Ioo interval induces a Tendsto relation from 𝓟(Iio a) to 𝓟(Iio a), capturing convergence within a left-bounded open region around a.

Русский

Пусть α — предобратство и a ∈ α. Интервал Ioo задаёт схождение от 𝓟(Iio a) к 𝓟(Iio a), фиксируя поведение слева от a.

LaTeX

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

Lean4

instance tendsto_Ioo_Iio_Iio {a : α} : TendstoIxxClass Ioo (𝓟 (Iio a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

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