instArchimedeanInt — Mathlib

English

The integers are Archimedean with respect to the usual order.

Русский

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

LaTeX

$$$$ \operatorname{Archimedean}(\mathbb{Z}). $$$$

Lean4

instance : Archimedean ℤ :=
  ⟨fun n m m0 =>
    ⟨n.toNat,
      le_trans (Int.self_le_toNat _) <| by
        simpa only [nsmul_eq_mul, zero_add, mul_one] using
          mul_le_mul_of_nonneg_left (Int.add_one_le_iff.2 m0) (Int.ofNat_zero_le n.toNat)⟩⟩

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