Denumerability of ℚ

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

instance Rat.instInfiniteRat : Infinite ℚ

Equations

• Rat.instInfiniteRat = ⋯

instance Rat.instDenumerableRat : Denumerable ℚ

Denumerability of the Rational Numbers

Equations

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

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