-- The rationals are countable
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Rat.Countable
import Cardinal.CountableClosure
import Defs
import Relation.QuotientOperations

theorem positiveNaturals.subset
  shows positiveNaturals ⊆ ℕ
proof
  intros n member
  obtain ⟨natural, nonzero⟩ := positiveNaturals.membership.forward with member
  exact natural

-- Representatives are pairs of a pair of naturals and a positive natural.
theorem rationalRepresentatives.countable
  shows Countable(rationalRepresentatives)
proof
  have naturals := naturals.countable
  have pairs : Countable(integerPairs)
    unfold integerPairs
    exact Countable.product with *
  have subset := positiveNaturals.subset
  have positives := Countable.subset with *
  unfold rationalRepresentatives
  exact Countable.product with *

-- ℚ is the image of the representatives under the quotient projection.
theorem rationals.countable
  shows Countable(ℚ)
proof
  have equivalence := rationalEquivalent.equivalence
  have surjection := quotientProjection.surjective with *
  have countable := rationalRepresentatives.countable
  unfold ℚ
  exact Countable.of_surjection with *