Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Checked.Aown330000340000

Aown 330000 340000 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Aown330000340000.fan14Owner0Part0 :
Certificates.FanWitness

Shared exact orientation-fan tail for this local exclusion.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown330000340000.excluded14_0 :
    Certificates.ExcludedOn (model14.B 0) 9000000000000 (model14.caps 0) (model14.ord 0) 0 1 100
    source
    theorem ConwaySoifer.Simplified.Certificates.Aown_330000_340000_checked :
    Data.Aown330000340000.Valid