exists_nat_pos_inv_lt — Mathlib

English

For any positive real b, there exists a natural number n with n > 0 such that n^{-1} < b.

Русский

Для любого положительного b существует натуральное число n, такое что 1/n < b.

LaTeX

$$$$\forall b>0,\\exists n\\in\\mathbb{N}, 0 < n \\wedge n^{-1} < b.$$$$

Lean4

theorem exists_nat_pos_inv_lt {b : ℝ} (hb : 0 < b) : ∃ (n : ℕ), 0 < n ∧ (n : ℝ)⁻¹ < b :=
  by
  refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_
  have := (inv_pos_of_pos hb).trans hk
  refine ⟨Nat.cast_pos.mp this, ?_⟩
  rwa [inv_lt_comm₀ this hb]

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