English
For an irrational x and a natural n, there exists a positive distance ε such that every integer m satisfies dist(x, m/n) ≥ ε.
Русский
Для иррационального x и натурального n существует положительное расстояние ε, такое что для каждого целого m расстояние |x − m/n| ≥ ε.
LaTeX
$$$\exists \varepsilon>0\;\forall m\in\mathbb{Z},\;\varepsilon\le |x-\tfrac{m}{n}|$$$
Lean4
theorem eventually_forall_le_dist_cast_div (hx : Irrational x) (n : ℕ) : ∀ᶠ ε : ℝ in 𝓝 0, ∀ m : ℤ, ε ≤ dist x (m / n) :=
by
have A : IsClosed (range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ)) :=
((isClosedMap_smul₀ (n⁻¹ : ℝ)).comp Int.isClosedEmbedding_coe_real.isClosedMap).isClosed_range
have B : x ∉ range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ) :=
by
rintro ⟨m, rfl⟩
simp at hx
rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩
refine (ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => ?_
rw [dist_comm] at hlt
refine hε (ball_subset_ball hδ hlt) ⟨m, ?_⟩
simp [div_eq_inv_mul]
