archimedean_iff_nat_le — Mathlib

English

Archimedean K is equivalent to: for every x there exists n ∈ ℕ with x ≤ n.

Русский

Архимедово свойство эквивалентно: для каждого x существует n ∈ ℕ такое, что x ≤ n.

LaTeX

$$$\\text{Archimedean } K \\iff \\forall x, \\exists n \\in \\mathbb{N}, x \\le n$$$

Lean4

theorem archimedean_iff_nat_le : Archimedean K ↔ ∀ x : K, ∃ n : ℕ, x ≤ n :=
  archimedean_iff_nat_lt.trans
    ⟨fun H x => (H x).imp fun _ => le_of_lt, fun H x =>
      let ⟨n, h⟩ := H x
      ⟨n + 1, lt_of_le_of_lt h (Nat.cast_lt.2 (lt_add_one _))⟩⟩

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