lean_workbook_plus_37505

Proved

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

Let $x\in ]0,1[$ \n\nProve that exists $\frac{a}{b}$ rational, $a,b$ positive integers, $gcd(a,b)=1$ , such that $|x-\frac{a}{b}|<\frac{1}{b^{2}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37505 (x : ℝ) (hx : 0 < x ∧ x < 1) :
    ∃ a b : ℤ, a > 0 ∧ b > 0 ∧ Int.gcd a b = 1 ∧ |x - a / b| < 1 / b^2   :=  by sorry

Source