OAI/Combinatorics/HadwigerCounterexample/BatchCharacters.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Batch Characters

  1. def OAI.HadwigerCounterexample.led line 15
  2. def OAI.HadwigerCounterexample.relay line 16
  3. theorem OAI.HadwigerCounterexample.led_uniform line 23
  4. theorem OAI.HadwigerCounterexample.led_piece line 29
  5. def OAI.HadwigerCounterexample.heard line 44
  6. theorem OAI.HadwigerCounterexample.heard_fresh line 47
  7. theorem OAI.HadwigerCounterexample.led_off_r line 58
  8. theorem OAI.HadwigerCounterexample.led_off_l line 68
  9. def OAI.HadwigerCounterexample.phot line 77
  10. theorem OAI.HadwigerCounterexample.light_bound line 81