OAI/Combinatorics/HadwigerCounterexample/BinaryStatusComparison.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Binary Status Comparison

  1. theorem OAI.HadwigerCounterexample.disagreement_bound line 13
  2. def OAI.HadwigerCounterexample.majority line 19
  3. theorem OAI.HadwigerCounterexample.majority_bound line 22
  4. theorem OAI.HadwigerCounterexample.majority_charge line 34
  5. theorem OAI.HadwigerCounterexample.reflect_cost line 49
  6. abbrev OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.Pulsar line 69
  7. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.shot line 72
  8. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.praise line 74
  9. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.counsel line 77
  10. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.amazes line 81
  11. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.amends line 82
  12. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.amendsB line 87
  13. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.splitCounsel line 90
  14. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.paeans line 107