archimedean_iff_rat_le — Mathlib

English

Let K be Archimedean. Then Archimedean is equivalent to: for every x in K, there exists a rational q with x ≤ q.

Русский

Пусть K Архимедово упорядоченное поле. Тогда Архимедово свойство эквивалентно: для каждого x ∈ K существует q ∈ ℚ such that x ≤ q.

LaTeX

$$$\operatorname{Archimedean}(K) \iff \forall x:K,\ \exists q\in\mathbb{Q},\ x \le q$$$

Lean4

theorem archimedean_iff_rat_le : Archimedean K ↔ ∀ x : K, ∃ q : ℚ, x ≤ q :=
  archimedean_iff_rat_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 (Rat.cast_lt.2 (lt_add_one _))⟩⟩

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