Grace/Cumulus/Real/Uncountable/PrefixBound.g17

Open in Workbench Download source

Imports

Digits · Nat.Order

Declarations

Source

1-- Uncountability of the Dedekind reals - PrefixBound2-- 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.PrefixBound8import Digits9import Nat.Order1011theorem cantorPrefix.lt_pow (X : Set, n : Nat)12  shows cantorPrefix(X, n) < 4 ^ n13proof14  induction n15  | zero =>16    have prefixShape := cantorPrefix.zero at X17    have powerShape := pow.zero at 418    rw prefixShape19    rw powerShape20    arith21  | succ(k) using ih =>22    have prefixShape := cantorPrefix.succ at X, k23    have powerShape := pow.succ at 4, k24    rw prefixShape25    rw powerShape26    have digitCases := binaryDigit.cases at X, k27    cases digitCases with zero | one28    . rw zero29      have productZero := mul.right_zero at 230      rw productZero31      have sumZero := add.right_unit at 4 * cantorPrefix(X, k)32      rw sumZero33      exact Less.mul_left at cantorPrefix(X, k), 4 ^ k, 4 with34        natural.four_nonzero, ih35    . rw one36      have productOne := mul.right_unit at 237      rw productOne38      have prefixNatural : Nat(cantorPrefix(X, k))39        apply cantorPrefix.natural at X, k40      have fourNatural : Nat(4)41        typecheck42      have powerNatural : Nat(4 ^ k)43        apply pow.closed at 4, k44      have leftNatural : Nat(4 * cantorPrefix(X, k))45        typecheck46      have rightNatural : Nat(4 * (4 ^ k))47        typecheck48      have leftReflexive : 4 * cantorPrefix(X, k) ≤ 4 * cantorPrefix(X, k)49        apply LessEqual.reflexive at 4 * cantorPrefix(X, k)50      have twoLessFour : 2 < 451        arith52      have gap : 4 * cantorPrefix(X, k) + 2 < 4 * cantorPrefix(X, k) + 453        apply LessEqual.add_Less at54          4 * cantorPrefix(X, k), 4 * cantorPrefix(X, k), 2, 455        . exact leftReflexive56        . exact twoLessFour57      have successorBound := ih58      have scaledBound : LessEqual(mul(4, succ(cantorPrefix(X, k))), mul(4, 4 ^ k))59        apply LessEqual.mul_left at succ(cantorPrefix(X, k)), 4 ^ k, 460        . exact successorBound61      have successorShape : 4 * succ(cantorPrefix(X, k)) =62        4 * cantorPrefix(X, k) + 463        ring64      rw successorShape at scaledBound65      apply Less.transitive_LessEqual at66        4 * cantorPrefix(X, k) + 2,67        4 * cantorPrefix(X, k) + 4,68        4 * (4 ^ k)69      . typecheck70      . typecheck71