mathlib documentation

data.rat.denumerable

Denumerability of ℚ #

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

@[instance]
@[instance]

Denumerability of the Rational Numbers

Equations
theorem cardinal.mk_rat  :