OAI/Combinatorics/VariableWL/PortGame.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.TypedGame.Preserved line 11
  2. def OAI.VariableWL.TypedGame.Compose line 16
  3. theorem OAI.VariableWL.TypedGame.Preserved.compose line 18
  4. theorem OAI.VariableWL.TypedGame.Preserved.flip line 36
  5. theorem OAI.VariableWL.TypedGame.adjacency_preserved line 42
  6. def OAI.VariableWL.TypedGame.SameTriangle line 47
  7. def OAI.VariableWL.TypedGame.Exit line 50
  8. def OAI.VariableWL.TypedGame.Access line 53
  9. def OAI.VariableWL.TypedGame.UnderlyingEdge line 55
  10. theorem OAI.VariableWL.TypedGame.sameTriangle_preserved line 58
  11. theorem OAI.VariableWL.TypedGame.exit_preserved line 66
  12. theorem OAI.VariableWL.TypedGame.access_preserved line 72
  13. theorem OAI.VariableWL.TypedGame.underlyingEdge_preserved line 76
  14. theorem OAI.VariableWL.SubcubicRealization.sameTriangle_iff line 87
  15. theorem OAI.VariableWL.SubcubicRealization.exit_iff line 106
  16. theorem OAI.VariableWL.SubcubicRealization.access_iff line 126
  17. theorem OAI.VariableWL.SubcubicRealization.underlyingEdge_iff line 138
  18. theorem OAI.VariableWL.SubcubicRealization.winning_color line 162
  19. def OAI.VariableWL.SubcubicRealization.SortWalk line 172
  20. theorem OAI.VariableWL.SubcubicRealization.winning_sortWalk line 177