Between_two_Real_Numbers_exists_Rational_Number

Proved

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

between-two-real-numbers-exists-rational-numberproofwikireal-analysis

Let $a, b \in \R$ be real numbers such that $a < b$ . Then $\exists r \in \Q: a < r < b$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Between_two_Real_Numbers_exists_Rational_Number (a b : ℝ) (h : a < b) : ∃ r : ℚ, a < (↑r : ℝ) ∧ (↑r : ℝ) < b := by sorry

Source

https://proofwiki.org/wiki/Between_two_Real_Numbers_exists_Rational_Number

View graph