English
The set of good rational approximations is infinite iff ξ is irrational.
Русский
Множество хороших рациональных приближений бесконечно тогда и только тогда, когда ξ иррационально.
LaTeX
$$$$\\{q∈\\mathbb{Q} : |ξ-q| < 1/(q.den)^2\\}.\\\\Infinite \\;\\iff\\; ξ\\;\\text{irrational}.$$$$
Lean4
/-- The set of good rational approximations to a real number `ξ` is infinite if and only if
`ξ` is irrational. -/
theorem infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational (ξ : ℝ) :
{q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2}.Infinite ↔ Irrational ξ :=
by
refine
⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b _ H => Set.not_infinite.mpr ?_ h,
Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩
convert Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b) with q
rw [H, (by (push_cast; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))]
norm_cast