OAI/Combinatorics/HadwigerCounterexample/FinitePhaseAlternative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite Phase Alternative

  1. def OAI.HadwigerCounterexample.maxSpan line 13
  2. structure OAI.HadwigerCounterexample.PhaseReady line 15
  3. def OAI.HadwigerCounterexample.voidFrame line 41
  4. theorem OAI.HadwigerCounterexample.framesCost line 44
  5. theorem OAI.HadwigerCounterexample.mark_bazaar line 70
  6. theorem OAI.HadwigerCounterexample.phase_alternative line 98