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]
Denumerability of the Rational Numbers
Equations
- rat.denumerable = let T : Type := {x // 0 < x.snd ∧ x.fst.nat_abs.coprime x.snd}, _inst : infinite T := rat.denumerable._proof_1, _inst_1 : encodable T := subtype.encodable, _inst_2 : denumerable T := denumerable.of_encodable_of_infinite T in denumerable.of_equiv T denumerable_aux