OAI/Combinatorics/HadwigerCounterexample/CrossPatternCounting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cross Pattern Counting

  1. abbrev OAI.HadwigerCounterexample.Avenue line 15
  2. def OAI.HadwigerCounterexample.interDraw line 16
  3. def OAI.HadwigerCounterexample.disperses line 19
  4. def OAI.HadwigerCounterexample.arcPeak line 21
  5. def OAI.HadwigerCounterexample.peak line 24
  6. theorem OAI.HadwigerCounterexample.peak_bdd line 27
  7. theorem OAI.HadwigerCounterexample.real_peak line 34
  8. theorem OAI.HadwigerCounterexample.peak_le line 42
  9. theorem OAI.HadwigerCounterexample.sized_peak line 46
  10. theorem OAI.HadwigerCounterexample.peak_pos line 56
  11. abbrev OAI.HadwigerCounterexample.Incident line 71
  12. def OAI.HadwigerCounterexample.took line 72
  13. theorem OAI.HadwigerCounterexample.took_same line 75
  14. abbrev OAI.HadwigerCounterexample.Bag line 110
  15. def OAI.HadwigerCounterexample.peakExpense line 111
  16. theorem OAI.HadwigerCounterexample.bagCount line 114
  17. theorem OAI.HadwigerCounterexample.price_peak line 133