left_nhdsWithin_Ioo_neBot — Mathlib

English

For a < b, the left-neighbourhood at a inside Ioo(a,b) is nontrivial; points of Ioo(a,b) approach a from the right.

Русский

Для a < b левая окрестность a внутри Ioo(a,b) ненулевая; точки Ioo(a,b) подходят к a справа.

LaTeX

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

Lean4

theorem left_nhdsWithin_Ioo_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ioo a b] a) :=
  (isGLB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)

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