mathlib documentation

data.rat.denumerable

Denumerability of ℚ #

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

@[protected, instance]
@[protected, instance]

Denumerability of the Rational Numbers

Equations
theorem cardinal.mk_rat  :