Grace/Cumulus/Real/Uncountable/Final.g17

Open in Workbench Download source

Imports

Encoding · Cardinal.Countable

Declarations

Source

1-- Uncountability of the Dedekind reals - Final2-- 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.Final8import Encoding9import Cardinal.Countable1011-- The Cantor-space embedding X ↦ cantorReal(X).12def cantorEmbedding : Set :=13  { p ∈ 𝒫(ℕ) × ℝ | ∃ X ∈ 𝒫(ℕ), p = (X ↦ cantorReal(X)) }1415theorem cantorEmbedding.relates (X A : Set)16  shows relates(cantorEmbedding, X, A) ↔17    (X ∈ 𝒫(ℕ) ∧ A = cantorReal(X))18proof19  constructor20  . intro related21    unfold relates at related22    simp [cantorEmbedding.membership] at related23    rcases related with ⟨bounded, Y, yInPower, shape⟩24    obtain ⟨xShape, aShape⟩ := orderedPair.injective with shape25    constructor26    . rw xShape27      exact yInPower28    . rw xShape29      exact aShape30  . intro data31    rcases data with ⟨xInPower, rfl⟩32    unfold relates33    apply cantorEmbedding.membership.backward34    constructor35    . apply product.pair at X, cantorReal(X), 𝒫(ℕ), ℝ36      . exact xInPower37      . exact cantorReal.real at X38    . witness X39      constructor40      . exact xInPower41      . rfl4243theorem cantorEmbedding.total44  shows TotalBetween(cantorEmbedding, 𝒫(ℕ), ℝ)45proof46  intros X xInPower47  witness cantorReal(X)48  constructor49  . exact cantorReal.real at X50  . apply cantorEmbedding.relates.backward at X, cantorReal(X)51    constructor52    . exact xInPower53    . rfl5455theorem cantorEmbedding.functional56  shows Functional(cantorEmbedding)57proof58  intros X A xA B xB59  have first := cantorEmbedding.relates.forward with xA60  have second := cantorEmbedding.relates.forward with xB61  rcases first with ⟨_, aShape⟩62  rcases second with ⟨_, bShape⟩63  have reverseB : cantorReal(X) = B64    rw bShape65    rfl66  calc67    A = cantorReal(X) := aShape68    _ = B := reverseB6970theorem cantorEmbedding.function71  shows cantorEmbedding : 𝒫(ℕ) → ℝ72proof73  constructor74    intros p member75    obtain ⟨bounded, witnesses⟩ := cantorEmbedding.membership.forward with member76    exact bounded77  . constructor78    . exact cantorEmbedding.functional79    . exact cantorEmbedding.total8081theorem cantorEmbedding.injective82  shows InjectiveBetween(cantorEmbedding, 𝒫(ℕ), ℝ)83proof84  constructor85  . exact cantorEmbedding.function86  . intros X xInPower Y yInPower A aInReal xMaps yMaps87    have xData := cantorEmbedding.relates.forward with xMaps88    have yData := cantorEmbedding.relates.forward with yMaps89    rcases xData with ⟨_, xShape⟩90    rcases yData with ⟨_, yShape⟩91    have reverseX : cantorReal(X) = A92      rw xShape93      rfl94    have sameReals : cantorReal(X) = cantorReal(Y)95      calc96        cantorReal(X) = A := reverseX97        _ = cantorReal(Y) := yShape98    have subsetX := powerset.membership_iff.forward with xInPower99    have subsetY := powerset.membership_iff.forward with yInPower100    exact cantorReal.injective with subsetX, subsetY, sameReals101102theorem reals.uncountable103  shows Uncountable(ℝ)104proof105  unfold Uncountable106  intro countable107  obtain ⟨f, realsIntoNaturals⟩ := countable108  have powersetIntoReals := cantorEmbedding.injective109  have composite := compose.injective with powersetIntoReals, realsIntoNaturals110  exact powerset.naturals_not_injects_into_naturals with composite111