nhdsLT_neBot — Mathlib

English

For any finite extended real x > 0, the left-hand neighborhood inside (−∞, x) around x is nontrivial; there are points just below x arbitrarily close to x.

Русский

Для любых конечных ENNReal x > 0 левая окрестность внутри (−∞, x) вокруг x непустая; существуют точки, близкие к x слева.

LaTeX

$$$(\\mathcal{N}_{<}(x)) \\neq \\bot$ for NeZero x$$

Lean4

@[instance]
theorem nhdsLT_neBot [NeZero x] : (𝓝[<] x).NeBot :=
  nhdsWithin_Iio_self_neBot' ⟨0, NeZero.pos x⟩

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