lt_iff_exists_real_btwn — Mathlib

English

Between any a < b in EReal there exists a real x with a < x and (x : EReal) < b.

Русский

Между любыми a < b в EReal существует вещественное число x such that a < x и (x : EReal) < b.

LaTeX

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

Lean4

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

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