right_nhdsWithin_Ico_neBot — Mathlib

English

For any a < b, the right-neighbourhood filter at b restricted to the half-open interval Ico(a,b) is nontrivial; i.e., one can approach b from below within Ico(a,b).

Русский

Пусть a < b. Тогда правая окрестность b внутри Ico(a,b) ненулевая; т.е. можно подходить к b снизу внутри Ico(a,b).

LaTeX

$$$\\mathcal{N}_{Ico(a,b)}(b) \\neq \\bot$$$

Lean4

theorem right_nhdsWithin_Ico_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b) :=
  (isLUB_Ico H).nhdsWithin_neBot (nonempty_Ico.2 H)

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