nhdsGT_zero_neBot — Mathlib

English

The right-neighborhood of 0 in the extended nonnegative reals is nontrivial; i.e., there exist points strictly greater than 0 that lie arbitrarily close to 0 from above.

Русский

Правобоковая окрестность нуля в расширенных неотрицательных вещественных числах не тождественно нуль; то есть существуют точки строго больше нуля, приближающиеся к нулю сверху.

LaTeX

$$$(\\mathcal{N}_{>[0]}(0)) \\neq \\bot$$$

Lean4

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

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