Documentation

LeanPool.ConwaySoifer.Simplified.Certificates.Checked.Sext210000220000

Sext 210000 220000 #

Kernel-checked forced assignments and closed-interval exclusions.

source
def ConwaySoifer.Simplified.Certificates.Sext210000220000.fan52Owner0Part0 :
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
    def ConwaySoifer.Simplified.Certificates.Sext210000220000.fan52Owner0Part1 :
    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.Sext210000220000.excluded52_0 :
      Certificates.ExcludedOn (model52.B 0) 9000000000000 (model52.caps 0) (model52.ord 0) 0 1 100
      source
      theorem ConwaySoifer.Simplified.Certificates.Sext_210000_220000_checked :
      Data.Sext210000220000.Valid