[GOAL]
⊢ Denumerable ℚ
[PROOFSTEP]
let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.coprime x.2 }
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
⊢ Denumerable ℚ
[PROOFSTEP]
letI : Infinite T := Infinite.of_injective _ denumerable_aux.injective
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
this : Infinite T := Infinite.of_injective (↑Rat.denumerable_aux) (Equiv.injective Rat.denumerable_aux)
⊢ Denumerable ℚ
[PROOFSTEP]
letI : Encodable T := Subtype.encodable
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
this✝ : Infinite T := Infinite.of_injective (↑Rat.denumerable_aux) (Equiv.injective Rat.denumerable_aux)
this : Encodable T := Subtype.encodable
⊢ Denumerable ℚ
[PROOFSTEP]
letI : Denumerable T := ofEncodableOfInfinite T
[GOAL]
T : Type := { x // 0 < x.snd ∧ Nat.coprime (Int.natAbs x.fst) x.snd }
this✝¹ : Infinite T := Infinite.of_injective (↑Rat.denumerable_aux) (Equiv.injective Rat.denumerable_aux)
this✝ : Encodable T := Subtype.encodable
this : Denumerable T := ofEncodableOfInfinite T
⊢ Denumerable ℚ
[PROOFSTEP]
exact Denumerable.ofEquiv T denumerable_aux
[GOAL]
⊢ #ℚ = ℵ₀
[PROOFSTEP]
simp only [mk_eq_aleph0]
