OAI/Combinatorics/VariableWL/SubcubicGame.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Subcubic.Vertex line 15
  2. abbrev OAI.VariableWL.Subcubic.graph line 16
  3. abbrev OAI.VariableWL.Subcubic.finiteGraph line 17
  4. def OAI.VariableWL.Subcubic.translation line 19
  5. def OAI.VariableWL.Subcubic.numberedTranslation line 23
  6. def OAI.VariableWL.Subcubic.numberedPart line 27
  7. theorem OAI.VariableWL.Subcubic.numberedTranslation_local line 30
  8. theorem OAI.VariableWL.Subcubic.winning_of_witness line 38
  9. abbrev OAI.VariableWL.Subcubic.Response line 74
  10. def OAI.VariableWL.Subcubic.zeroQuery line 76
  11. def OAI.VariableWL.Subcubic.valuationQuery line 79
  12. theorem OAI.VariableWL.Subcubic.valuationQuery_injective line 84
  13. theorem OAI.VariableWL.Subcubic.decode_winning line 95
  14. theorem OAI.VariableWL.Subcubic.zeroQuery_recognized line 104
  15. theorem OAI.VariableWL.Subcubic.zeroQuery_agree line 118
  16. def OAI.VariableWL.Subcubic.attainedRings line 162
  17. theorem OAI.VariableWL.Subcubic.consistent_of_winning line 184
  18. theorem OAI.VariableWL.Subcubic.block_nonempty line 191
  19. theorem OAI.VariableWL.Subcubic.positive_order line 195
  20. theorem OAI.VariableWL.Subcubic.connected line 201
  21. theorem OAI.VariableWL.Subcubic.degree_le_three line 206
  22. theorem OAI.VariableWL.Subcubic.equal_order line 216
  23. theorem OAI.VariableWL.Subcubic.promise line 219
  24. theorem OAI.VariableWL.Subcubic.equivalent_iff_consistent line 230