OAI/Combinatorics/HadwigerCounterexample/PhaseAlternativeSupport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Phase Alternative Support

  1. theorem OAI.HadwigerCounterexample.onW_ne line 15
  2. theorem OAI.HadwigerCounterexample.on_law line 20
  3. theorem OAI.HadwigerCounterexample.onW_true line 22
  4. theorem OAI.HadwigerCounterexample.on_both line 25
  5. theorem OAI.HadwigerCounterexample.pr_shield line 32
  6. def OAI.HadwigerCounterexample.rhUp line 37
  7. theorem OAI.HadwigerCounterexample.bySide_on line 38
  8. def OAI.HadwigerCounterexample.scaleBill line 49
  9. def OAI.HadwigerCounterexample.tonalMix line 52
  10. def OAI.HadwigerCounterexample.tonalTiny line 54
  11. theorem OAI.HadwigerCounterexample.pitch_turn line 58
  12. theorem OAI.HadwigerCounterexample.tonal_left line 65
  13. theorem OAI.HadwigerCounterexample.glimpse_sub line 71
  14. def OAI.HadwigerCounterexample.preGlimpse line 86
  15. theorem OAI.HadwigerCounterexample.glimpse_cover_failure line 89
  16. theorem OAI.HadwigerCounterexample.Bazaar.cover_options line 113