Grace/Cumulus/Cardinal/CountableClosure.g17

Open in Workbench Download source

Imports

Countable · Product

Declarations

Source

1-- Countable sets are closed under subsets, images, and finite products2-- 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.CountableClosure8import Countable9import Product1011-- A subset of a countable set is countable: restrict the injection.12theorem Countable.subset (A S : Set)13  requires countable : Countable(A)14  requires subset : S ⊆ A15  shows Countable(S)16proof17  obtain ⟨g, injection⟩ := countable18  have function := Injective.function with injection19  have closed : ∀ x ∈ S, g(x) ∈ ℕ20    intros x hx21    have hxA := subset with x, hx22    exact FunctionBetween.apply_closed at g, A, ℕ, x with *23  have restricted := restrict.function with *24  witness restrict(g, S)25  constructor26  . exact restricted27  . intros x hx y hy z hz relatesX relatesY28    have dataX := restrict.relates.forward with relatesX29    have dataY := restrict.relates.forward with relatesY30    rcases dataX with ⟨_, gX⟩31    rcases dataY with ⟨_, gY⟩32    have hxA := subset with x, hx33    have hyA := subset with y, hy34    exact Injective.cancel with *3536-- The codes an injection g assigns to the preimages of b under f.37def surjectionCodes (g f A b : Set) : Set :=38  { n ∈ ℕ | ∃ a ∈ A, relates(f, a, b) ∧ g(a) = n }3940theorem surjectionCodes.subset (g f A b : Set)41  shows surjectionCodes(g, f, A, b) ⊆ ℕ42proof43  simp4445theorem surjectionCodes.nonempty (g f A B b : Set)46  requires injection : InjectiveBetween(g, A, ℕ)47  requires surjection : SurjectiveBetween(f, A, B)48  requires member : b ∈ B49  shows Nonempty(surjectionCodes(g, f, A, b))50proof51  have gFunction := Injective.function with injection52  rcases surjection with ⟨fFunction, onto⟩53  obtain ⟨a, ha, relatesA⟩ := onto with b, member54  have code := FunctionBetween.apply_closed at g, A, ℕ, a with *55  witness g(a)56  apply surjectionCodes.membership.backward57  constructor58  . exact code59  . witness a60    refine ⟨ha, relatesA, rfl⟩6162-- Send each b to the least code of a preimage. Choosing the least code63-- needs no Choice axiom.64defgraph surjectionCode (g f A B : Set) (b ∈ B) : ℕ := leastNatural(surjectionCodes(g, f, A, b))65requires injection : InjectiveBetween(g, A, ℕ)66requires surjection : SurjectiveBetween(f, A, B)67proof68  have inhabited := surjectionCodes.nonempty with *69  have naturals := surjectionCodes.subset at g, f, A, b70  have selected := leastNatural.selected at surjectionCodes(g, f, A, b) with *71  exact selected.left7273-- The image of a countable set under a surjection is countable.74theorem Countable.of_surjection (f A B : Set)75  requires countable : Countable(A)76  requires surjection : SurjectiveBetween(f, A, B)77  shows Countable(B)78proof79  obtain ⟨g, injection⟩ := countable80  have gFunction := Injective.function with injection81  have fFunction := Surjective.function with surjection82  have functional := FunctionBetween.functional with fFunction83  have codeFunction := surjectionCode.function at g, f, A, B with *84  witness surjectionCode(g, f, A, B)85  constructor86  . exact codeFunction87  . intros b1 hb1 b2 hb2 z hz relates1 relates288    have value1 := FunctionBetween.apply_value at surjectionCode(g, f, A, B), B, ℕ, b1, z with *89    have value2 := FunctionBetween.apply_value at surjectionCode(g, f, A, B), B, ℕ, b2, z with *90    have code1 := surjectionCode.value at g, f, A, B, b1 with *91    have code2 := surjectionCode.value at g, f, A, B, b2 with *92    have inhabited1 := surjectionCodes.nonempty with hb193    have inhabited2 := surjectionCodes.nonempty with hb294    have naturals1 := surjectionCodes.subset at g, f, A, b195    have naturals2 := surjectionCodes.subset at g, f, A, b296    have least1 := leastNatural.member at surjectionCodes(g, f, A, b1) with *97    have least2 := leastNatural.member at surjectionCodes(g, f, A, b2) with *98    have data1 := surjectionCodes.membership.forward with least199    have data2 := surjectionCodes.membership.forward with least2100    obtain ⟨_, a1, ha1, relatesF1, codeA1⟩ := data1101    obtain ⟨_, a2, ha2, relatesF2, codeA2⟩ := data2102    have sameCode : g(a2) = g(a1) by cc103    have gRelates1 := FunctionBetween.relates_apply at g, A, ℕ, a1 with *104    have gRelates2 := FunctionBetween.relates_apply at g, A, ℕ, a2 with *105    rw sameCode at gRelates2106    have codeNatural := FunctionBetween.apply_closed at g, A, ℕ, a1 with *107    have sameInput := Injective.cancel with ha1, ha2108    rw sameInput at relatesF1109    exact Functional.unique with *110111-- Two to the power of n is never zero.112theorem pow.two_nonzero (n : Nat)113  shows 2 ^ n ≠ 0114proof115  induction n116  | zero =>117    rw pow.zero118    intro bad119    have positiveOne : 0 < 1 by arith120    rw bad at positiveOne121    exact Less.irreflexive with *, positiveOne122  | succ(k) using ih =>123    rw pow.succ124    have twoNonzero : 2 ≠ 0125      intro bad126      have positiveTwo : 0 < 2 by arith127      rw bad at positiveTwo128      exact Less.irreflexive at 0 with *, positiveTwo129    exact mul.nonzero at 2, 2 ^ k with *130131-- The code 2^a · (2b + 1) determines a and b: a is the number of factors of132-- two, and 2b + 1 is the odd part.133theorem pairingCode.strict (a k b d : Nat)134  requires equal : 2 ^ a * succ(b + b) = 2 ^ (succ(a) + k) * succ(d + d)135  shows ⊥136proof137  have split := pow.add at 2, k, succ(a) with *138  rw split at equal139  have step := pow.succ at 2, a with *140  rw step at equal141  have rearranged : (2 * 2 ^ a) * 2 ^ k * succ(d + d) = 2 ^ a * (2 * (2 ^ k * succ(d + d))) by ring142  rw rearranged at equal143  have nonzero := pow.two_nonzero at a with *144  have cancelled := mul.left_cancel_positive with *145  have doubled := mul.two_left at 2 ^ k * succ(d + d) with *146  rw doubled at cancelled147  have even := Even.double at 2 ^ k * succ(d + d) with *148  rw ← cancelled at even149  have odd := Odd.double_successor at b with *150  exact Odd.not_even with *, even151152theorem pairingCode.injective (a b c d : Nat)153  requires equal : 2 ^ a * succ(b + b) = 2 ^ c * succ(d + d)154  shows a = c ∧ b = d155proof156  have twoNonzero : 2 ≠ 0157    intro bad158    arith159  have shape := Less.trichotomy at a, c with *160  rcases shape with less | same | greater161  . exfalso162    obtain ⟨k, kNat, cShape⟩ := less163    rw ← cShape at equal164    exact pairingCode.strict with equal165  . rw same at equal166    have nonzero := pow.two_nonzero at c with *167    have cancelled := mul.left_cancel_positive with *168    have doubles := Naturals.injective.succ at b + b, d + d with *169    have bLe : b ≤ d by arith170    have dLe : d ≤ b by arith171    exact ⟨same, (LessEqual.antisymmetric at b, d with *)⟩172  . exfalso173    obtain ⟨k, kNat, aShape⟩ := greater174    rw ← aShape at equal175    symm at equal176    exact pairingCode.strict with equal177178-- The code of a pair of naturals.179defunique pairingCode (p : Set) (n ∈ ℕ) :=180  ∃ a ∈ ℕ, ∃ b ∈ ℕ, p = (a, b) ∧ n = 2 ^ a * succ(b + b)181requires pair : p ∈ ℕ × ℕ182proof183  obtain ⟨bound, a, ha, b, hb, shape⟩ := product.membership.forward with pair184  have aNat := nat.omega.backward with ha185  have bNat := nat.omega.backward with hb186  have codeNat : Nat(2 ^ a * succ(b + b)) by typecheck187  have codeMember := nat.omega.forward with codeNat188  refine ⟨2 ^ a * succ(b + b), codeMember, a, ha, b, hb, shape, rfl⟩189uniqueness190  intros u hu first v hv second191  obtain ⟨a, ha, b, hb, shapeU, valueU⟩ := first192  obtain ⟨c, hc, d, hd, shapeV, valueV⟩ := second193  have equal : (a, b) = (c, d) by cc194  obtain ⟨ac, bd⟩ := orderedPair.injective with equal195  rw [valueU, valueV, ac, bd]196  rfl197198defgraph naturalPairing (p ∈ ℕ × ℕ) : ℕ := pairingCode(p)199proof200  have selected := pairingCode.selected with member201  exact selected.left202203theorem naturalPairing.injective204  shows InjectiveBetween(naturalPairing, ℕ × ℕ, ℕ)205proof206  have function := naturalPairing.function207  constructor208  . exact function209  . intros p hp q hq z hz relatesP relatesQ210    have valueP := FunctionBetween.apply_value at naturalPairing, ℕ × ℕ, ℕ, p, z with *211    have valueQ := FunctionBetween.apply_value at naturalPairing, ℕ × ℕ, ℕ, q, z with *212    have codeP := naturalPairing.value with hp213    have codeQ := naturalPairing.value with hq214    have selectedP := pairingCode.selected with hp215    have selectedQ := pairingCode.selected with hq216    obtain ⟨_, a, ha, b, hb, shapeP, formP⟩ := selectedP217    obtain ⟨_, c, hc, d, hd, shapeQ, formQ⟩ := selectedQ218    have aNat := nat.omega.backward with ha219    have bNat := nat.omega.backward with hb220    have cNat := nat.omega.backward with hc221    have dNat := nat.omega.backward with hd222    have same : 2 ^ a * succ(b + b) = 2 ^ c * succ(d + d) by cc223    have coordinates := pairingCode.injective with *224    rcases coordinates with ⟨ac, bd⟩225    rw [shapeP, shapeQ, ac, bd]226    rfl227228-- The product of two countable sets is countable.229theorem Countable.product (A B : Set)230  requires countableA : Countable(A)231  requires countableB : Countable(B)232  shows Countable(A × B)233proof234  obtain ⟨g, injectionG⟩ := countableA235  obtain ⟨h, injectionH⟩ := countableB236  have product := productMap.injective at g, h, A, B, ℕ, ℕ with *237  have pairing := naturalPairing.injective238  have composed := compose.injective at naturalPairing, productMap(g, h, A, B, ℕ, ℕ), A × B, ℕ × ℕ, ℕ with *239  witness compose(naturalPairing, productMap(g, h, A, B, ℕ, ℕ), A × B, ℕ × ℕ, ℕ)240  exact composed241242theorem naturals.countable243  shows Countable(ℕ)244proof245  witness identity(ℕ)246  exact identity.injective247