OAI/Combinatorics/HadwigerCounterexample/RelationMismatchBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Relation Mismatch Bounds

  1. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.seeking line 20
  2. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.any_label line 22
  3. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.generic_apt line 28
  4. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.plenitude line 32
  5. structure OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.RhymeSet line 54
  6. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.RhymeSet.read line 60
  7. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.RhymeSet.soot line 63
  8. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.leftChime line 66
  9. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.rightChime line 68
  10. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.dual_eq line 71
  11. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.charge line 88
  12. def OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.outstraps line 92
  13. theorem OAI.HadwigerCounterexample.StatusAnalysis.DualAnalysis.charge_counter line 96