nhdsLT_neBot — Mathlib

English

If a densely ordered set has no minimum element, then for every a the left-neighbourhood filter 𝒩_{<}(a) is nontrivial; in other words, there are points less than a arbitrarily close to a from the left.

Русский

Пусть множество с плотной упорядоченностью не имеет минимума. Тогда для каждого a левая окрестность 𝒩_{<}(a) не тривиальна; т.е. существуют точки меньше a, стремящиеся к a слева.

LaTeX

$$$\\mathcal{N}_{<}(a) \\neq \\bot$$$

Lean4

instance nhdsLT_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) :=
  nhdsWithin_Iio_neBot (le_refl a)

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