Grace/Cumulus/Real/Uncountable/Cut.g17

Open in Workbench Download source

Imports

Approximation

Declarations

• cantorReal def
• cantorReal.real theorem derivation

Source

1-- Uncountability of the Dedekind reals - Cut2-- 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.Cut8import Approximation910-- The real coded by X is the lower closure of all its finite endpoints.11def cantorReal (X : Set) : Set :=12  { q ∈ ℚ | ∃ n ∈ ℕ, relates(rationalLess, q, cantorApprox(X, n)) }1314theorem cantorReal.real (X : Set)15  shows Real(cantorReal(X))16proof17  apply Real.characterization.backward18  constructor19    intros q member20    have shape := cantorReal.membership at X, q21    obtain ⟨qRational, witnessData⟩ := shape.forward with member22    exact qRational23  constructor24  . have zeroRational := rationalZero.rational25    obtain ⟨below, belowRational, belowZero⟩ := rationalLess.exists_below with zeroRational26    witness below27    have shape := cantorReal.membership at X, below28    apply shape.backward29    constructor30    . exact belowRational31    . witness 032      constructor33      . exact nat.omega.forward at 0 with Naturals.constructor.zero34      . rw cantorApprox.zero35        exact belowZero36  constructor37  . intro allRationals38    have oneInCut : rationalOne ∈ cantorReal(X)39      rw allRationals40      exact rationalOne.rational41    have oneShape := cantorReal.membership at X, rationalOne42    obtain ⟨oneRationalAgain, n, nNatural, oneBelow⟩ :=43      oneShape.forward with oneInCut44    have nNat := nat.omega.backward with nNatural45    have endpointBelowOne : cantorApprox(X, n) < rationalOne by apply cantorApprox.below_one46    have cycle := rationalLess.transitive with oneBelow, endpointBelowOne47    have irreflexive := rationalLess.irreflexive_on48    exact irreflexive with rationalOne, oneRationalAgain, cycle49  constructor50  . intros q qInCut p pRational pBelowQ51    have qShape := cantorReal.membership at X, q52    obtain ⟨qRational, m, mNatural, qBelowEndpoint⟩ :=53      qShape.forward with qInCut54    have mNat := nat.omega.backward with mNatural55    have pBelowEndpoint := rationalLess.transitive with pBelowQ, qBelowEndpoint56    have pShape := cantorReal.membership at X, p57    apply pShape.backward58    constructor59    . exact pRational60    . refine ⟨m, mNatural, pBelowEndpoint⟩61  . intros q qInCut62    have qShape := cantorReal.membership at X, q63    obtain ⟨qRationalAgain, k, kNatural, qBelowEndpointAgain⟩ :=64      qShape.forward with qInCut65    have kNat := nat.omega.backward with kNatural66    have endpointRationalK : Rational(cantorApprox(X, k)) by apply cantorApprox.rational67    have qRationalClass : Rational(q) by exact qRationalAgain68    obtain ⟨r, rRational, qBelowR, rBelowEndpoint⟩ := rationalLess.dense with69      qRationalClass, endpointRationalK, qBelowEndpointAgain70    witness r71    constructor72    . have rShape := cantorReal.membership at X, r73      apply rShape.backward74      constructor75      . exact rRational76      . refine ⟨k, kNatural, rBelowEndpoint⟩77    . exact qBelowR78