le_iff_forall_rat_lt_imp_le — Mathlib

English

Let K be a field with a linear order that is Archimedean. For all x, y in K, x ≤ y if and only if every rational q satisfies: if q < x then q ≤ y.

Русский

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

LaTeX

$$$$ x \le y \iff \forall q \in \mathbb{Q},\ (q : K) < x \rightarrow (q : K) \le y. $$$$

Lean4

theorem le_iff_forall_rat_lt_imp_le : x ≤ y ↔ ∀ q : ℚ, (q : K) < x → (q : K) ≤ y :=
  ⟨fun hxy _ hqx ↦ hqx.le.trans hxy, le_of_forall_rat_lt_imp_le⟩

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