lean_workbook_plus_11727

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given any two real numbers $x<y$ , prove that we can find a rational number $q$ such that $x<q<y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11727 (x y : ℝ) (h : x < y) : ∃ q : ℚ, x < q ∧ ↑q < y   :=  by sorry

Source