OAI/Combinatorics/HadwigerCounterexample/UnaryCellComparisons.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Unary Cell Comparisons

  1. def OAI.HadwigerCounterexample.Template.curtain line 17
  2. def OAI.HadwigerCounterexample.Template.propel line 19
  3. abbrev OAI.HadwigerCounterexample.Template.Localist line 22
  4. def OAI.HadwigerCounterexample.Template.board line 24
  5. def OAI.HadwigerCounterexample.Template.shadowed line 27
  6. def OAI.HadwigerCounterexample.Template.astonish line 30
  7. def OAI.HadwigerCounterexample.Template.exceeds line 33
  8. theorem OAI.HadwigerCounterexample.Template.astonish_val line 38
  9. structure OAI.HadwigerCounterexample.Template.Paint line 45
  10. def OAI.HadwigerCounterexample.Template.Paint.cost line 48
  11. def OAI.HadwigerCounterexample.Template.mural line 50
  12. def OAI.HadwigerCounterexample.Template.design line 51
  13. def OAI.HadwigerCounterexample.Template.patched line 54
  14. theorem OAI.HadwigerCounterexample.Template.design_mono line 60
  15. def OAI.HadwigerCounterexample.Template.paintJoin line 84
  16. theorem OAI.HadwigerCounterexample.Template.join_cost line 90
  17. theorem OAI.HadwigerCounterexample.Template.design_patch line 110