Grace/Cumulus/Cardinal/Countable.g17

Open in Workbench Download source

Imports

Finite

Declarations

• Countable predicate
• Uncountable predicate
• cantorDiagonal def
• cantorDiagonal.subset theorem derivation
• cantorDiagonal.in_powerset theorem derivation
• Cantor.no_surjection_onto_powerset theorem derivation
• powerset.not_equipotent theorem derivation
• countableDiagonal def
• countableDiagonal.subset theorem derivation
• powerset.naturals_not_injects_into_naturals theorem derivation
• powerset.naturals_uncountable theorem derivation

Source

1-- Countability and Cantor's diagonal theorem2-- 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.Cardinal.Countable8import Finite910-- A set is countable when it injects into the natural numbers. This includes11-- finite sets and gives the usual "at most countable" convention.12predicate Countable (A : Set) := ∃ f, InjectiveBetween(f, A, ℕ)13predicate Uncountable (A : Set) := ¬Countable(A)1415-- The diagonal subset associated with a proposed enumeration of P(A).16def cantorDiagonal (f A : Set) : Set :=17  { x ∈ A | ¬(x ∈ f(x)) }1819theorem cantorDiagonal.subset (f A : Set)20  shows cantorDiagonal(f, A) ⊆ A21proof22  simp2324theorem cantorDiagonal.in_powerset (f A : Set)25  shows cantorDiagonal(f, A) ∈ 𝒫(A)26proof27  simp [Subset, set.powerset, cantorDiagonal.subset]2829-- Cantor's theorem in its graph-theoretic form: no set-valued function from A30-- onto its powerset exists. The proof is the literal diagonal argument.31theorem Cantor.no_surjection_onto_powerset (f A : Set)32  shows ¬SurjectiveBetween(f, A, 𝒫(A))33proof34  intro surjective35  rcases surjective with ⟨function, onto⟩36  have diagonalInPower := cantorDiagonal.in_powerset at f, A37  specialize onto with cantorDiagonal(f, A), diagonalInPower38  obtain ⟨d, dInA, mapsToDiagonal⟩ := onto39  have value := FunctionBetween.apply_value with function, dInA, mapsToDiagonal40  have diagonalShape := cantorDiagonal.membership at f, A, d41  have membershipCases : d ∈ cantorDiagonal(f, A) ∨ ¬(d ∈ cantorDiagonal(f, A)) by tauto42  cases membershipCases with diagonal | notDiagonal43  . have shape := diagonalShape.forward with diagonal44    rcases shape with ⟨dInAAgain, notInValue⟩45    rw value at notInValue46    exact notInValue with diagonal47  . apply notDiagonal48    apply diagonalShape.backward49    constructor50    . exact dInA51    . rw value52      exact notDiagonal5354theorem powerset.not_equipotent (A : Set)55  shows ¬(A ≃ 𝒫(A))56proof57  intro equivalent58  obtain ⟨f, bijective⟩ := equivalent59  have surjective := Bijective.surjective with bijective60  exact Cantor.no_surjection_onto_powerset with surjective6162-- The injection form of Cantor's theorem for the naturals. Given a proposed63-- code f : P(N) → N, diagonalize at the code assigned to the diagonal set.64def countableDiagonal (f : Set) : Set :=65  { n ∈ ℕ | ∃ X ∈ 𝒫(ℕ), relates(f, X, n) ∧ ¬(n ∈ X) }6667theorem countableDiagonal.subset (f : Set)68  shows countableDiagonal(f) ⊆ ℕ69proof70  simp7172theorem powerset.naturals_not_injects_into_naturals (f : Set)73  shows ¬InjectiveBetween(f, 𝒫(ℕ), ℕ)74proof75  intro injection76  rcases injection with ⟨function, oneToOne⟩77  have diagonalSubset := countableDiagonal.subset at f78  have diagonalInPower := set.powerset.backward at countableDiagonal(f), ℕ with79    diagonalSubset80  obtain ⟨d, dInN, diagonalMaps⟩ := FunctionBetween.exists_value with function, diagonalInPower81  have cases : d ∈ countableDiagonal(f) ∨ ¬(d ∈ countableDiagonal(f)) by tauto82  cases cases with member | missing83  . have data := countableDiagonal.membership.forward at84      f, d with member85    rcases data with ⟨valueNatural, X, xInPower, xMaps, valueMissingX⟩86    have sameSet := oneToOne with87      X, xInPower, countableDiagonal(f), diagonalInPower,88      d, dInN,89      xMaps, diagonalMaps90    apply valueMissingX91    rwa sameSet92  . apply missing93    apply countableDiagonal.membership.backward94    constructor95    . exact dInN96    . witness countableDiagonal(f)97      constructor98      . exact diagonalInPower99      . constructor100        . exact diagonalMaps101        . exact missing102103theorem powerset.naturals_uncountable104  shows Uncountable(𝒫(ℕ))105proof106  unfold Uncountable107  intro countable108  obtain ⟨f, injection⟩ := countable109  exact powerset.naturals_not_injects_into_naturals with injection110