English
Let a be a positive extended nonnegative real number (a ≠ 0). Then there exists a natural number n with the inverse of n, viewed as an extended nonnegative real, strictly smaller than a.
Русский
Пусть a — положительное число из расширенного множества неотрицательных вещественных чисел; тогда существует натуральное число n такое, что n⁻¹ < a.
LaTeX
$$$\\forall a \\in \\mathbb{R}_{\\ge 0}^{\\infty}, a \\neq 0 \\Rightarrow \\exists n \\in \\mathbb{N}, \\; (n : \\mathbb{R}_{\\ge 0}^{\\infty})^{-1} < a$$$
Lean4
theorem exists_inv_nat_lt {a : ℝ≥0∞} (h : a ≠ 0) : ∃ n : ℕ, (n : ℝ≥0∞)⁻¹ < a :=
inv_inv a ▸ by simp only [ENNReal.inv_lt_inv, ENNReal.exists_nat_gt (inv_ne_top.2 h)]
