Denumerability of ℚ

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

instance Rat.instInfiniteRat : Infinite ℚ

Equations

• Rat.instInfiniteRat = Rat.instInfiniteRat.proof_1

instance Rat.instDenumerableRat : Denumerable ℚ

Denumerability of the Rational Numbers

Equations

• Rat.instDenumerableRat = let T := { x // 0 < x.snd ∧ Nat.Coprime (Int.natAbs x.fst) x.snd }; Denumerable.ofEquiv T Rat.denumerable_aux

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