lean_workbook_plus_8873

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that for any positive real number $\epsilon$ , there exists an integer $n$ such that $\frac{1}{n}< \epsilon$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8873 (ε : ℝ) (hε : 0 < ε) : ∃ n : ℤ, (1 : ℝ) / n < ε   :=  by sorry

Source