OAI/Combinatorics/HadwigerCounterexample/SyntheticSliceExperiments.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Synthetic Slice Experiments

  1. abbrev OAI.HadwigerCounterexample.Punch line 13
  2. abbrev OAI.HadwigerCounterexample.Gauge line 14
  3. def OAI.HadwigerCounterexample.gaugeAddr line 15
  4. def OAI.HadwigerCounterexample.usesPunch line 16
  5. instance OAI.HadwigerCounterexample.(instance at line 18) line 18
  6. abbrev OAI.HadwigerCounterexample.Tickets line 20
  7. def OAI.HadwigerCounterexample.punchField line 21
  8. def OAI.HadwigerCounterexample.issued line 23
  9. def OAI.HadwigerCounterexample.rung line 25
  10. def OAI.HadwigerCounterexample.ticketsFee line 27
  11. theorem OAI.HadwigerCounterexample.ticketsFee_pos line 28
  12. theorem OAI.HadwigerCounterexample.rungPrice line 30
  13. theorem OAI.HadwigerCounterexample.ticketLaw line 64
  14. theorem OAI.HadwigerCounterexample.ticketFlow line 66
  15. theorem OAI.HadwigerCounterexample.ticketCap line 76
  16. def OAI.HadwigerCounterexample.tabGram line 80
  17. theorem OAI.HadwigerCounterexample.tabGram_sound line 83