Documentation
LeanPool
.
HadwigerNelsonBounds
.
PartsGadgetHardVerification0
Search
return to top
source
Imports
Init
LeanPool.HadwigerNelsonBounds.PartsGadgetHardCasesData
Imported by
HadwigerNelsonBounds
.
partsGadgetHardCertificate0_verifies
HadwigerNelsonBounds
.
partsGadgetHardCertificate1_verifies
HadwigerNelsonBounds
.
partsGadgetHardCertificate2_verifies
HadwigerNelsonBounds
.
partsGadgetHardCertificate3_verifies
Kernel checks for hard-case certificate group 0.
source
theorem
HadwigerNelsonBounds
.
partsGadgetHardCertificate0_verifies
:
partsGadgetHardCertificate0
.
Verifies
source
theorem
HadwigerNelsonBounds
.
partsGadgetHardCertificate1_verifies
:
partsGadgetHardCertificate1
.
Verifies
source
theorem
HadwigerNelsonBounds
.
partsGadgetHardCertificate2_verifies
:
partsGadgetHardCertificate2
.
Verifies
source
theorem
HadwigerNelsonBounds
.
partsGadgetHardCertificate3_verifies
:
partsGadgetHardCertificate3
.
Verifies