eventually_forall_le_dist_cast_div_of_denom_le

English

For an irrational x and n, there is a neighborhood near 0 such that for all k ≤ n and all m ∈ ℤ, dist(x, m/k) ≥ ε for some ε > 0.

Русский

Для иррационального x и натурального n существует окрестность нуля, где для всех 1 ≤ k ≤ n и всех m ∈ ℤ расстояние |x − m/k| ≥ ε.

LaTeX

$$$\exists \varepsilon>0\;\forall k\le n\;\forall m\in\mathbb{Z},\;\varepsilon\le |x-\tfrac{m}{k}|$$$

Lean4

theorem eventually_forall_le_dist_cast_div_of_denom_le (hx : Irrational x) (n : ℕ) :
    ∀ᶠ ε : ℝ in 𝓝 0, ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (m / k) :=
  (finite_le_nat n).eventually_all.2 fun k _ => hx.eventually_forall_le_dist_cast_div k

Похожие утверждения