Denumerability of ℚ

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

instance Rat.instInfiniteRat : Infinite ℚ

instance Rat.instDenumerableRat : Denumerable ℚ

Denumerability of the Rational Numbers

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