nhdsGT_ofNat_neBot — Mathlib

English

For any natural number n (viewed inside ENNReal via the cast), the upper neighborhood is nontrivial; i.e., there exist elements strictly above n that can be approached from above.

Русский

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

LaTeX

$$$(\\mathcal{N}_{>[n]}(n)) \\neq \\bot$ where $n$ is viewed in ENNReal$$

Lean4

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

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