Commit 2023-06-19 08:58 cc29b553

View on Github →

feat: port Archive.Wiedijk100Theorems.CubingACube (#5201)

Estimated changes

Modified Archive.lean

Created Archive/Wiedijk100Theorems/CubingACube.lean

added theorem Theorems100.«82».Correct.b_add_w_le_one

added theorem Theorems100.«82».Correct.nontrivial_fin

added theorem Theorems100.«82».Correct.shiftUp_bottom_subset_bottoms

added theorem Theorems100.«82».Correct.side_subset

added theorem Theorems100.«82».Correct.toSet_subset_unitCube

added theorem Theorems100.«82».Correct.w_ne_one

added theorem Theorems100.«82».Correct.zero_le_b

added theorem Theorems100.«82».Correct.zero_le_of_mem

added theorem Theorems100.«82».Correct.zero_le_of_mem_side

added structure Theorems100.«82».Correct

added theorem Theorems100.«82».Cube.b_lt_xm

added theorem Theorems100.«82».Cube.b_mem_bottom

added theorem Theorems100.«82».Cube.b_mem_side

added theorem Theorems100.«82».Cube.b_mem_toSet

added theorem Theorems100.«82».Cube.b_ne_xm

added def Theorems100.«82».Cube.bottom

added theorem Theorems100.«82».Cube.head_shiftUp

added theorem Theorems100.«82».Cube.hw'

added def Theorems100.«82».Cube.shiftUp

added def Theorems100.«82».Cube.side

added theorem Theorems100.«82».Cube.side_nonempty

added theorem Theorems100.«82».Cube.side_tail

added theorem Theorems100.«82».Cube.side_unitCube

added theorem Theorems100.«82».Cube.tail_shiftUp

added def Theorems100.«82».Cube.toSet

added theorem Theorems100.«82».Cube.toSet_disjoint

added theorem Theorems100.«82».Cube.toSet_subset

added def Theorems100.«82».Cube.unitCube

added theorem Theorems100.«82».Cube.univ_pi_side

added def Theorems100.«82».Cube.xm

added structure Theorems100.«82».Cube

added theorem Theorems100.«82».Ico_lemma

added def Theorems100.«82».OnBoundary

added def Theorems100.«82».Valley

added theorem Theorems100.«82».b_le_b

added def Theorems100.«82».bcubes

added theorem Theorems100.«82».bottom_mem_side

added theorem Theorems100.«82».cannot_cube_a_cube

added def Theorems100.«82».decreasingSequence

added theorem Theorems100.«82».exists_mi

added theorem Theorems100.«82».injective_sequenceOfCubes

added def Theorems100.«82».mi

added theorem Theorems100.«82».mi_mem_bcubes

added theorem Theorems100.«82».mi_minimal

added theorem Theorems100.«82».mi_not_onBoundary'

added theorem Theorems100.«82».mi_not_onBoundary

added theorem Theorems100.«82».mi_strict_minimal

added theorem Theorems100.«82».mi_xm_ne_one

added theorem Theorems100.«82».nonempty_bcubes

added theorem Theorems100.«82».nontrivial_bcubes

added theorem Theorems100.«82».not_correct

added theorem Theorems100.«82».smallest_onBoundary

added theorem Theorems100.«82».strictAnti_sequenceOfCubes

added theorem Theorems100.«82».t_le_t

added theorem Theorems100.«82».tail_sub

added theorem Theorems100.«82».valley_mi

added theorem Theorems100.«82».valley_unitCube

added theorem Theorems100.«82».w_lt_w