OAI/Combinatorics/HadwigerCounterexample/ScalarStatusAlgebra.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Scalar Status Algebra

  1. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Nodes line 13
  2. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Grid line 14
  3. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Cell line 15
  4. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Par line 17
  5. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Whole line 18
  6. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Signal line 20
  7. abbrev OAI.HadwigerCounterexample.StatusAnalysis.View line 21
  8. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Question line 22
  9. def OAI.HadwigerCounterexample.StatusAnalysis.view line 25
  10. def OAI.HadwigerCounterexample.StatusAnalysis.testV line 29
  11. def OAI.HadwigerCounterexample.StatusAnalysis.want line 33
  12. def OAI.HadwigerCounterexample.StatusAnalysis.couple line 35
  13. def OAI.HadwigerCounterexample.StatusAnalysis.coverBase line 40
  14. theorem OAI.HadwigerCounterexample.StatusAnalysis.testV_surj line 41
  15. theorem OAI.HadwigerCounterexample.StatusAnalysis.coversFull line 44
  16. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Rates line 47
  17. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Suite line 48
  18. abbrev OAI.HadwigerCounterexample.StatusAnalysis.LedgerS line 49
  19. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Cabinet line 50
  20. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Quota line 51
  21. abbrev OAI.HadwigerCounterexample.StatusAnalysis.Court line 52
  22. abbrev OAI.HadwigerCounterexample.StatusAnalysis.StatusSp line 53
  23. def OAI.HadwigerCounterexample.StatusAnalysis.separate line 56
  24. def OAI.HadwigerCounterexample.StatusAnalysis.speak line 64
  25. theorem OAI.HadwigerCounterexample.StatusAnalysis.speak_solo line 67
  26. def OAI.HadwigerCounterexample.StatusAnalysis.scorecard line 78
  27. structure OAI.HadwigerCounterexample.StatusAnalysis.Critic line 81
  28. def OAI.HadwigerCounterexample.StatusAnalysis.Counter line 85
  29. theorem OAI.HadwigerCounterexample.StatusAnalysis.vanishes line 89
  30. theorem OAI.HadwigerCounterexample.StatusAnalysis.counter_score line 98
  31. theorem OAI.HadwigerCounterexample.StatusAnalysis.critic_nz line 147