eq_of_forall_lt_rat_iff_lt — Mathlib

English

If for every rational q, x < q is equivalent to y < q, then x = y.

Русский

Если для каждого рационального q верно, что x < q эквивалентно y < q, то x = y.

LaTeX

$$$$\bigl(\forall q \in \mathbb{Q},\ x < q \leftrightarrow y < q\bigr) \Rightarrow x = y.$$$$

Lean4

theorem eq_of_forall_lt_rat_iff_lt (h : ∀ q : ℚ, x < q ↔ y < q) : x = y :=
  (le_of_forall_lt_rat_imp_le fun q hq => ((h q).2 hq).le).antisymm <|
    le_of_forall_lt_rat_imp_le fun q hq => ((h q).1 hq).le

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