eventually_forall_le_dist_cast_rat_of_den_le

English

For an irrational x, and for each n, there exists ε > 0 such that for all rationals r with denom ≤ n, dist(x, r) ≥ ε.

Русский

Для иррационального x и любого n существует ε > 0 такое, что для всех рациональных r с знаменателем ≤ n расстояние dist(x, r) ≥ ε.

LaTeX

$$$\forall x\in\mathbb{R},\operatorname{Irrational}(x)\Rightarrow\forall n\in\mathbb{N},\exists \varepsilon>0\;\forall r\in\mathbb{Q}, r.den\le n\Rightarrow \varepsilon\le d(x,r.cast)$$$

Lean4

theorem eventually_forall_le_dist_cast_rat_of_den_le (hx : Irrational x) (n : ℕ) :
    ∀ᶠ ε : ℝ in 𝓝 0, ∀ r : ℚ, r.den ≤ n → ε ≤ dist x r :=
  (hx.eventually_forall_le_dist_cast_div_of_denom_le n).mono fun ε H r hr => by
    simpa only [Rat.cast_def] using H r.den hr r.num

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