OAI/Combinatorics/VariableWL/GeneralGame.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.General.Base line 12
  2. abbrev OAI.VariableWL.General.Part line 13
  3. abbrev OAI.VariableWL.General.Vertex line 15
  4. def OAI.VariableWL.General.owner line 18
  5. def OAI.VariableWL.General.IsBase line 21
  6. def OAI.VariableWL.General.Shared line 24
  7. def OAI.VariableWL.General.Agree line 27
  8. def OAI.VariableWL.General.BaseAdj line 31
  9. theorem OAI.VariableWL.General.baseAdj_symm line 34
  10. def OAI.VariableWL.General.graph line 39
  11. def OAI.VariableWL.General.partEquiv line 56
  12. def OAI.VariableWL.General.baseEquiv line 60
  13. def OAI.VariableWL.General.vertexEquiv line 64
  14. theorem OAI.VariableWL.General.owner_vertexEquiv line 69
  15. theorem OAI.VariableWL.General.baseAdj_translate line 73
  16. theorem OAI.VariableWL.General.adjacency_translate line 91
  17. def OAI.VariableWL.General.leafCount line 104
  18. def OAI.VariableWL.General.finiteGraph line 107
  19. theorem OAI.VariableWL.General.equal_orders line 115
  20. theorem OAI.VariableWL.Game.winning_reached line 126
  21. theorem OAI.VariableWL.Game.Winning.neighborhood_bijection line 140
  22. theorem OAI.VariableWL.Game.Winning.degree_eq line 161
  23. def OAI.VariableWL.General.baseVertex line 181
  24. def OAI.VariableWL.General.leafVertex line 182
  25. def OAI.VariableWL.General.splitVertex line 185
  26. theorem OAI.VariableWL.General.baseVertex_owner line 191
  27. theorem OAI.VariableWL.General.leafVertex_injective line 198
  28. theorem OAI.VariableWL.General.baseVertex_injective line 204
  29. theorem OAI.VariableWL.General.exists_leaf_of_owner line 208
  30. theorem OAI.VariableWL.General.leaf_adj_iff line 217
  31. theorem OAI.VariableWL.General.leaf_degree line 231
  32. def OAI.VariableWL.General.baseNeighbors line 238
  33. theorem OAI.VariableWL.General.base_degree line 273
  34. def OAI.VariableWL.Game.active line 284
  35. theorem OAI.VariableWL.Game.mem_active line 287
  36. theorem OAI.VariableWL.Game.active_card_le line 297
  37. theorem OAI.VariableWL.Game.active_card_lt_vacant line 301
  38. theorem OAI.VariableWL.Game.active_mono line 311
  39. theorem OAI.VariableWL.Game.active_update_subset line 317
  40. theorem OAI.VariableWL.Game.winning_of_block_families line 330