mathlib documentation

data.rat.denumerable

Denumerability of ℚ #

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

@[instance]
@[instance]
Equations