lt_iff_exists_rat_btwn — Mathlib

English

For any a < b in EReal, a < b iff there exists q ∈ ℚ with a < (q : ℝ) and (q : ℝ) < b.

Русский

Для любых a < b в EReal, a < b эквивалентно существованию q ∈ ℚ с a < (q : ℝ) и (q : ℝ) < b.

LaTeX

$$$ a < b \iff \exists q \in \mathbb{Q}, a < (q : \mathbb{R}) \land ((q : \mathbb{R}) : \mathrm{EReal}) < b $$$

Lean4

theorem lt_iff_exists_rat_btwn {a b : EReal} : a < b ↔ ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b :=
  ⟨fun hab => exists_rat_btwn_of_lt hab, fun ⟨_x, ax, xb⟩ => ax.trans xb⟩

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