nhdsGT_nat_neBot — Mathlib

English

For every natural number n, the neighborhood above n in ENNReal is nontrivial; i.e., there are elements strictly greater than n that lie arbitrarily close to n from above.

Русский

Для каждого натурального числа n окрестность над n в ENNReal непустая; существуют элементы строго большего, чем n, близко к n снизу.

LaTeX

$$$(\\mathcal{N}_{>[0]}(n)) \\neq \\bot$ for all $n \\in \\mathbb{N}$$$

Lean4

@[instance]
theorem nhdsGT_nat_neBot (n : ℕ) : (𝓝[>] (n : ℝ≥0∞)).NeBot :=
  nhdsGT_coe_neBot

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