tendsto_Ioo_Ioi_Ioi — Mathlib

English

For a preorder α and a ∈ α, the Ioo interval induces a Tendsto relation from 𝓟(Ioi a) to 𝓟(Ioi a), describing convergence within a rightward region beyond a.

Русский

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

LaTeX

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

Lean4

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

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