$|\mathbb Z|=|\mathbb Q|<|\mathbb R|$

Proved

ContinuumHypothesis.int_rat_equinumerous_lt_real

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

cardinal-arithmeticset-theory

The rationals can be put in one-to-one correspondence with the integers, while (Cantor) the set of integers has strictly smaller cardinality than the set of real numbers:

|\mathbb Z|=|\mathbb Q|\quad\text{and}\quad|\mathbb Z|<|\mathbb R|.

This is the observation that motivates the continuum hypothesis.

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem int_rat_equinumerous_lt_real : #ℤ = #ℚ ∧ #ℤ < #ℝ := by sorry

end ContinuumHypothesis

Source

Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Cardinality of infinite sets', paragraphs 2–3.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

∣Z∣=∣Q∣<∣R∣|\mathbb Z|=|\mathbb Q|<|\mathbb R|∣Z∣=∣Q∣<∣R∣

$|\mathbb Z|=|\mathbb Q|<|\mathbb R|$