nhdsWithin_Ioi_neBot — Mathlib

English

In any densely ordered space with no maximum, for any a, the right-neighborhood 𝓝_{> a}^? is nontrivial.

Русский

В плотно упорядоченном пространстве без максимума правая окрестность не тривиальна для любого a.

LaTeX

$$$NeBot\bigl(\mathcal{N}_{>a}(a)\bigr)$$$

Lean4

theorem nhdsWithin_Ioi_neBot [NoMaxOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Ioi a] b) :=
  nhdsWithin_Ioi_neBot' nonempty_Ioi H

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