OAI/Combinatorics/HadwigerCounterexample/EndpointEvaluations.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Endpoint Evaluations

  1. abbrev OAI.HadwigerCounterexample.Template.SameDuet line 17
  2. abbrev OAI.HadwigerCounterexample.Template.OppDuet line 19
  3. abbrev OAI.HadwigerCounterexample.Template.Chorus line 20
  4. instance OAI.HadwigerCounterexample.Template.(instance at line 21) line 21
  5. instance OAI.HadwigerCounterexample.Template.(instance at line 22) line 22
  6. def OAI.HadwigerCounterexample.Template.verses line 24
  7. def OAI.HadwigerCounterexample.Template.choral line 25
  8. abbrev OAI.HadwigerCounterexample.Template.Crossing line 51
  9. abbrev OAI.HadwigerCounterexample.Template.Harm line 53
  10. def OAI.HadwigerCounterexample.Template.Abbey line 54
  11. instance OAI.HadwigerCounterexample.Template.(instance at line 57) line 57
  12. instance OAI.HadwigerCounterexample.Template.(instance at line 60) line 60
  13. def OAI.HadwigerCounterexample.Template.monks line 62
  14. def OAI.HadwigerCounterexample.Template.croon line 69
  15. def OAI.HadwigerCounterexample.Template.chime line 71
  16. def OAI.HadwigerCounterexample.Template.chorusM line 75
  17. theorem OAI.HadwigerCounterexample.Template.chime_seq line 79
  18. theorem OAI.HadwigerCounterexample.Template.chorus_same line 87
  19. theorem OAI.HadwigerCounterexample.Template.chorus_cross line 97