OAI/Combinatorics/HadwigerCounterexample/LabeledGenerators.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Labeled Generators

  1. structure OAI.HadwigerCounterexample.StatusAnalysis.Club line 15
  2. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Straps line 20
  3. def OAI.HadwigerCounterexample.StatusAnalysis.Club.zone line 23
  4. def OAI.HadwigerCounterexample.StatusAnalysis.Club.band line 24
  5. def OAI.HadwigerCounterexample.StatusAnalysis.Club.bundle line 25
  6. def OAI.HadwigerCounterexample.StatusAnalysis.Club.contents line 27
  7. def OAI.HadwigerCounterexample.StatusAnalysis.Club.length3 line 29
  8. def OAI.HadwigerCounterexample.StatusAnalysis.Club.ration line 31
  9. def OAI.HadwigerCounterexample.StatusAnalysis.Club.yield3 line 33
  10. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.band_write line 37
  11. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.band_contents line 40
  12. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.length3_zero line 43
  13. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.zone_smaller line 47
  14. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.ration_le line 50
  15. def OAI.HadwigerCounterexample.StatusAnalysis.Club.addrs line 55
  16. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.yield_after line 57
  17. def OAI.HadwigerCounterexample.StatusAnalysis.Club.different line 65
  18. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.different_ne line 67
  19. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.bundle_one line 69
  20. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.bundle_insert line 75
  21. theorem OAI.HadwigerCounterexample.StatusAnalysis.Club.ration_eq line 90