Documentation

Mathlib.Data.Rat.Denumerable

Denumerability of ℚ #

This file proves that ℚ is denumerable.

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

source
instance Rat.instDenumerable :
Denumerable ℚ

Denumerability of the Rational Numbers

Equations