instDenselyNormedField — Mathlib

English

ℚ is densely normed: between any two real numbers there is a rational number with corresponding norm.

Русский

ℚ плотно нормировано: между любой парой вещественных чисел существует рациональное число с соответствующей нормой.

LaTeX

$$$\text{Rat.instDenselyNormedField}$: ∀ r1 < r2, ∃ q ∈ ℚ with r1 < q.cast < r2.$$

Lean4

instance instDenselyNormedField : DenselyNormedField ℚ where
  lt_norm_lt r₁ r₂ h₀
    hr :=
    let ⟨q, h⟩ := exists_rat_btwn hr
    ⟨q, by rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]⟩

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