Documentation
LeanPool
.
ConwaySoifer
.
Simplified
.
Certificates
.
Checked
.
Across092500097500
Search
return to top
source
Imports
Init
Mathlib.Tactic.FinCases
LeanPool.ConwaySoifer.Simplified.Certificates.Checkpoints.Across092500097500
LeanPool.ConwaySoifer.Simplified.Certificates.Steps.Across0925000975000
Imported by
ConwaySoifer
.
Simplified
.
Certificates
.
Across092500097500
.
excluded5_1
ConwaySoifer
.
Simplified
.
Certificates
.
Across_092500_097500_checked
Across 092500 097500
#
Kernel-checked forced assignments and closed-interval exclusions.
source
theorem
ConwaySoifer
.
Simplified
.
Certificates
.
Across092500097500
.
excluded5_1
:
Certificates.ExcludedOn
(
model5
.
B
1
)
9000000000000
(
model5
.
caps
1
)
(
model5
.
ord
1
)
0
1
200
source
theorem
ConwaySoifer
.
Simplified
.
Certificates
.
Across_092500_097500_checked
:
Data.Across092500097500
.
Valid