OAI/Combinatorics/HadwigerCounterexample/AmbientBatchSlots.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Ambient Batch Slots

  1. theorem OAI.HadwigerCounterexample.mapW_equiv_val line 16
  2. theorem OAI.HadwigerCounterexample.unif_equiv line 24
  3. theorem OAI.HadwigerCounterexample.on_equiv line 27
  4. abbrev OAI.HadwigerCounterexample.PlusRack line 34
  5. abbrev OAI.HadwigerCounterexample.Rack line 35
  6. def OAI.HadwigerCounterexample.sectionR line 36
  7. abbrev OAI.HadwigerCounterexample.Route line 38
  8. abbrev OAI.HadwigerCounterexample.Port line 39
  9. abbrev OAI.HadwigerCounterexample.Network line 40
  10. def OAI.HadwigerCounterexample.rackEquiv line 46
  11. abbrev OAI.HadwigerCounterexample.GeoM line 55
  12. def OAI.HadwigerCounterexample.gramPart line 57
  13. def OAI.HadwigerCounterexample.injPart line 60
  14. def OAI.HadwigerCounterexample.bothPart line 64
  15. def OAI.HadwigerCounterexample.scoreR line 66
  16. theorem OAI.HadwigerCounterexample.part_scores line 69
  17. theorem OAI.HadwigerCounterexample.both_test line 76
  18. theorem OAI.HadwigerCounterexample.pi_unif line 79
  19. theorem OAI.HadwigerCounterexample.pi_unifOn line 86
  20. def OAI.HadwigerCounterexample.rackStation line 97
  21. def OAI.HadwigerCounterexample.rackWave line 98
  22. theorem OAI.HadwigerCounterexample.station_split line 100
  23. def OAI.HadwigerCounterexample.netSize line 109
  24. def OAI.HadwigerCounterexample.netFact line 110
  25. theorem OAI.HadwigerCounterexample.netFact_pos line 114
  26. theorem OAI.HadwigerCounterexample.net_norm line 116
  27. theorem OAI.HadwigerCounterexample.wave_norm line 148
  28. theorem OAI.HadwigerCounterexample.injPart_failure line 154