Denumerability of ℚ

This file proves that ℚ is denumerable.

The fact that ℚ has cardinality ℵ₀ is proved in Data.Rat.Cardinal

instance Rat.instDenumerable : Denumerable ℚ

Denumerability of the Rational Numbers

Equations

• Rat.instDenumerable = Denumerable.ofEncodableOfInfinite ℚ