instArchimedean — Mathlib

English

The nonnegative rational numbers form an Archimedean ordered structure.

Русский

Ненегативные рациональные числа образуют архимедово упорядоченную структуру.

LaTeX

$$$$ \text{Archimedean} (\mathrm{NNRat}). $$$$

Lean4

instance instArchimedean [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Archimedean M] :
    Archimedean { x : M // 0 ≤ x } :=
  ⟨fun x y hy =>
    let ⟨n, hr⟩ := Archimedean.arch (x : M) (hy : (0 : M) < y)
    ⟨n, mod_cast hr⟩⟩

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