Grace/Cumulus/Real/Uncountable/Encoding.g17

Open in Workbench Download source

Imports

Separation

Declarations

• cantorPrefix.eq_of_real_eq theorem derivation
• cantorReal.injective theorem derivation

Source

1-- Uncountability of the Dedekind reals - Encoding2-- 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.Real.Uncountable.Encoding8import Separation910theorem cantorPrefix.eq_of_real_eq (X Y : Set, n : Nat)11  requires same : cantorReal(X) = cantorReal(Y)12  shows cantorPrefix(X, n) = cantorPrefix(Y, n)13proof14  induction n15  | zero =>16    have right : 0 = cantorPrefix(Y, 0)17      have rightShape := cantorPrefix.zero at Y18      rw rightShape19      rfl20    calc21      cantorPrefix(X, 0) = 0 := cantorPrefix.zero at X22      _ = cantorPrefix(Y, 0) := right23  | succ(k) using ih =>24    have leftShape := cantorPrefix.succ at X, k25    have rightShape := cantorPrefix.succ at Y, k26    rw [leftShape, rightShape, ih]27    have xCases := binaryDigit.cases at X, k28    have yCases := binaryDigit.cases at Y, k29    cases xCases with xZero | xOne30    . cases yCases with yZero | yOne31      . rw [xZero, yZero]32        rfl33      . exfalso34        have yMember : k ∈ Y35          by_contra yMissing36          have zeroAtY := binaryDigit.zero with yMissing37          rw yOne at zeroAtY38          have zeroNotOne := Naturals.disjoint.zero.succ at 039          apply zeroNotOne40          rw zeroAtY41          rfl42        have xMissing : ¬(k ∈ X)43          intro xMember44          have oneAtX := binaryDigit.one with xMember45          rw xZero at oneAtX46          exact Naturals.disjoint.zero.succ at 0 with oneAtX47        have bitY : k ∈ Y ↔ cantorMid(Y, k) ∈ cantorReal(Y) by apply cantorReal.bit48        have yMid := bitY.forward with yMember49        have midsEqual : cantorMid(X, k) = cantorMid(Y, k) by simp [cantorMid, ih]50        rw [← midsEqual, ← same] at yMid51        exact cantorMid.not_mem_of_missing with xMissing, yMid52    . cases yCases with yZero | yOne53      . exfalso54        have xMember : k ∈ X55          by_contra xMissing56          have zeroAtX := binaryDigit.zero with xMissing57          rw xOne at zeroAtX58          have zeroNotOne := Naturals.disjoint.zero.succ at 059          apply zeroNotOne60          rw zeroAtX61          rfl62        have yMissing : ¬(k ∈ Y)63          intro yMember64          have oneAtY := binaryDigit.one with yMember65          rw yZero at oneAtY66          exact Naturals.disjoint.zero.succ at 0 with oneAtY67        have bitX : k ∈ X ↔ cantorMid(X, k) ∈ cantorReal(X) by apply cantorReal.bit68        have xMid := bitX.forward with xMember69        have midsEqual : cantorMid(X, k) = cantorMid(Y, k) by simp [cantorMid, ih]70        rw [midsEqual, same] at xMid71        exact cantorMid.not_mem_of_missing with yMissing, xMid72      . rw [xOne, yOne]73        rfl7475theorem cantorReal.injective (X Y : Set)76  requires subsetX : X ⊆ ℕ77  requires subsetY : Y ⊆ ℕ78  requires same : cantorReal(X) = cantorReal(Y)79  shows X = Y80proof81  ext n82  constructor83  . intro memberX84    have nInOmega := subsetX with n, memberX85    have nNatural := nat.omega.backward with nInOmega86    have bitX : n ∈ X ↔ cantorMid(X, n) ∈ cantorReal(X) by apply cantorReal.bit87    have midpoint := bitX.forward with memberX88    have prefixesEqual := cantorPrefix.eq_of_real_eq with same89    have midsEqual : cantorMid(X, n) = cantorMid(Y, n) by simp [cantorMid, prefixesEqual]90    rw [midsEqual, same] at midpoint91    have bitY : n ∈ Y ↔ cantorMid(Y, n) ∈ cantorReal(Y) by apply cantorReal.bit92    exact bitY.backward with midpoint93  . intro memberY94    have nInOmega := subsetY with n, memberY95    have nNatural := nat.omega.backward with nInOmega96    have bitY : n ∈ Y ↔ cantorMid(Y, n) ∈ cantorReal(Y) by apply cantorReal.bit97    have midpoint := bitY.forward with memberY98    have prefixesEqual := cantorPrefix.eq_of_real_eq with same99    have midsEqual : cantorMid(X, n) = cantorMid(Y, n) by simp [cantorMid, prefixesEqual]100    rw [← midsEqual, ← same] at midpoint101    have bitX : n ∈ X ↔ cantorMid(X, n) ∈ cantorReal(X) by apply cantorReal.bit102    exact bitX.backward with midpoint103