archimedean_iff_rat_lt — Mathlib

English

Let K be a field with a linear order that is Archimedean. Then Archimedean is equivalent to: for every x in K there exists a rational q with x < q.

Русский

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

LaTeX

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

Lean4

theorem archimedean_iff_rat_lt : Archimedean K ↔ ∀ x : K, ∃ q : ℚ, x < q
    where
  mp _
    x :=
    let ⟨n, h⟩ := exists_nat_gt x
    ⟨n, by rwa [Rat.cast_natCast]⟩
  mpr
    H :=
    archimedean_iff_nat_lt.2 fun x ↦
      let ⟨q, h⟩ := H x;
      ⟨⌈q⌉₊, lt_of_lt_of_le h <| mod_cast Nat.le_ceil _⟩

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