OAI/Combinatorics/HadwigerCounterexample/SinglePositionExpansion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Single Position Expansion

  1. abbrev OAI.HadwigerCounterexample.Aside line 16
  2. def OAI.HadwigerCounterexample.chair line 17
  3. theorem OAI.HadwigerCounterexample.chair_split line 19
  4. theorem OAI.HadwigerCounterexample.chair_weight line 26
  5. def OAI.HadwigerCounterexample.arm line 33
  6. theorem OAI.HadwigerCounterexample.chair_arm line 35
  7. def OAI.HadwigerCounterexample.Template.beyond line 48
  8. def OAI.HadwigerCounterexample.Template.chairK line 50
  9. def OAI.HadwigerCounterexample.Template.chairI line 53
  10. theorem OAI.HadwigerCounterexample.Template.key_quoin line 57
  11. theorem OAI.HadwigerCounterexample.Template.key_split line 68
  12. def OAI.HadwigerCounterexample.Template.earns line 74