OAI/Computability/VertexCover/PCP/ZigzagGraphs.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.involutionEquiv line 14
  2. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 20
  3. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.squareFirst line 27
  4. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 31
  5. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.squareSwap line 37
  6. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 39
  7. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.square line 43
  8. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.square_rot_apply line 51
  9. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.square_next line 57
  10. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.cloudFirst line 60
  11. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 65
  12. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.crossCloud line 72
  13. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 75
  14. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.zigzag line 81
  15. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 89
  16. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 97
  17. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 100
  18. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 104
  19. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 107
  20. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 110
  21. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.cloudOperator line 117
  22. def OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.graphPermutation line 120
  23. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 123
  24. theorem OAI.UniqueGames.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 132