Denumerability of ℚ

This file proves that ℚ is infinite, denumerable, and deduces that it has cardinality omega.

instance Rat.instInfinite : Infinite ℚ

Equations

• Rat.instInfinite = ⋯

instance Rat.instDenumerable : Denumerable ℚ

Denumerability of the Rational Numbers

Equations

• Rat.instDenumerable = let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.Coprime x.2 }; Denumerable.ofEquiv T Rat.denumerable_aux

theorem Cardinal.mkRat : Cardinal.mk ℚ = Cardinal.aleph0