exists_nat_one_div_lt — Mathlib

English

For every ε > 0 in a suitable Archimedean field, there exists n ∈ ℕ with 1/(n+1) < ε.

Русский

Для каждого ε > 0 в архимедовом полем существует n ∈ ℕ такое, что 1/(n+1) < ε.

LaTeX

$$$\\exists n \\in \\mathbb{N}, \\; \\frac{1}{n+1} < \\varepsilon$$$

Lean4

theorem exists_nat_one_div_lt (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1 : K) < ε :=
  by
  obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)
  use n
  rw [div_lt_iff₀, ← div_lt_iff₀' hε]
  · apply hn.trans
    simp [zero_lt_one]
  · exact n.cast_add_one_pos

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