mathlib3 documentation

data.rat.denumerable

Denumerability of ℚ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Denumerability of the Rational Numbers

Equations