Rational numbers of bounded denominator in a bounded set

A bounded set of real numbers contains only finitely many rational numbers whose denominator is at most a given bound N: such a rational r is determined by the pair (r.num, r.den), and both coordinates are bounded. This is the finiteness behind the fact that infinitely many rational approximations to a real number must have unbounded denominators.

Main results

• Bornology.IsBounded.finite_setOf_rat_den_le: for a bounded s ⊆ ℝ and N : ℕ, the rationals r with r.den ≤ N and (r : ℝ) ∈ s form a finite set.

theorem Bornology.IsBounded.finite_setOf_rat_den_le {s : Set ℝ} (hs : IsBounded s) (N : ℕ) : {r : ℚ | r.den ≤ N ∧ ↑r ∈ s}.Finite

A bounded set of real numbers contains only finitely many rational numbers of denominator at most N.