nhdsGT_one_neBot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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