OAI/Combinatorics/IndependentSets/Expansion/Finite.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTransport.operator_reindex line 13
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTransport.energy_reindex line 22
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTransport.reindex_spectralCertificate line 26
  4. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.involutionEquiv line 52
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 58
  6. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.squareFirst line 65
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 69
  8. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.squareSwap line 75
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 77
  10. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.square line 81
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.square_rot_apply line 89
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.square_next line 95
  13. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.cloudFirst line 98
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 103
  15. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.crossCloud line 110
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 113
  17. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.zigzag line 119
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 127
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 135
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 138
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 142
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 145
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 148
  24. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.cloudOperator line 155
  25. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.graphPermutation line 158
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 161
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 170