exists_nat_gt — Mathlib

English

For any finite ENNReal r ≠ ∞, there exists a natural number n with r < n.

Русский

Для любого конечного ENNReal r, отличного от ∞, существует натуральное n, такое что r < n.

LaTeX

$$$ \text{ENNReal.exists_nat_gt} \{ r : \\mathbb{R}_{\\ge 0}^\\infty \} (h : r \neq \infty) : \exists n : \\mathbb{N}, r < n $$$

Lean4

protected theorem exists_nat_gt {r : ℝ≥0∞} (h : r ≠ ∞) : ∃ n : ℕ, r < n :=
  by
  lift r to ℝ≥0 using h
  rcases exists_nat_gt r with ⟨n, hn⟩
  exact ⟨n, coe_lt_natCast.2 hn⟩

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