exists_rat_near — Mathlib

English

For any x and ε > 0, there exists a rational q with |x - q| < ε.

Русский

Для любых x и ε > 0 существует рациональное q такое, что |x - q| < ε.

LaTeX

$$$$ \exists q \in \mathbb{Q},\ |x - q| < \varepsilon. $$$$

Lean4

theorem exists_rat_near (x : K) (ε0 : 0 < ε) : ∃ q : ℚ, |x - q| < ε :=
  let ⟨q, h₁, h₂⟩ := exists_rat_btwn <| ((sub_lt_self_iff x).2 ε0).trans ((lt_add_iff_pos_left x).2 ε0)
  ⟨q, abs_sub_lt_iff.2 ⟨sub_lt_comm.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩

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