Grace/Cumulus/Rat/Countable.g17

Open in Workbench Download source

Imports

Cardinal.CountableClosure · Defs · Relation.QuotientOperations

Declarations

• positiveNaturals.subset theorem derivation
• rationalRepresentatives.countable theorem derivation
• rationals.countable theorem derivation

Source

1-- The rationals are countable2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Rat.Countable8import Cardinal.CountableClosure9import Defs10import Relation.QuotientOperations1112theorem positiveNaturals.subset13  shows positiveNaturals ⊆ ℕ14proof15  intros n member16  obtain ⟨natural, nonzero⟩ := positiveNaturals.membership.forward with member17  exact natural1819-- Representatives are pairs of a pair of naturals and a positive natural.20theorem rationalRepresentatives.countable21  shows Countable(rationalRepresentatives)22proof23  have naturals := naturals.countable24  have pairs : Countable(integerPairs)25    unfold integerPairs26    exact Countable.product with *27  have subset := positiveNaturals.subset28  have positives := Countable.subset with *29  unfold rationalRepresentatives30  exact Countable.product with *3132-- ℚ is the image of the representatives under the quotient projection.33theorem rationals.countable34  shows Countable(ℚ)35proof36  have equivalence := rationalEquivalent.equivalence37  have surjection := quotientProjection.surjective with *38  have countable := rationalRepresentatives.countable39  unfold ℚ40  exact Countable.of_surjection with *41