exists_irrational_btwn — Mathlib

English

There exists an irrational number between any two real numbers x < y.

Русский

Между любыми двумя вещественными числами x < y существует иррациональное число.

LaTeX

$$$\forall x,y \in \mathbb{R},\ x < y \Rightarrow \exists r \in \mathbb{R}, \operatorname{Irrational}(r) \land x < r \land r < y$$$

Lean4

/-- There is an irrational number `r` between any two reals `x < r < y`. -/
theorem exists_irrational_btwn {x y : ℝ} (h : x < y) : ∃ r, Irrational r ∧ x < r ∧ r < y :=
  let ⟨q, ⟨hq1, hq2⟩⟩ := exists_rat_btwn ((sub_lt_sub_iff_right (√2)).mpr h)
  ⟨q + √2, irrational_sqrt_two.ratCast_add _, sub_lt_iff_lt_add.mp hq1, lt_sub_iff_add_lt.mp hq2⟩

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