OAI/Combinatorics/IndependentSets/Expansion/PreprocessingOverlayWords.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.row line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.trueRelation line 15
  3. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.oldReverseMap line 17
  4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.expanderReverseMap line 18
  5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.oldRow line 20
  6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow line 26
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.relation_ext line 31
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_old line 38
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_expander line 51
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_reverse_val line 67
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_reverse_val line 75
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_words line 83
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_words line 90
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.ofFn_overlayPorts line 100
  15. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows line 106
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_length line 110
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.flatRows_overlay line 114
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_words line 124
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.tableWords_overlay line 147
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.tableBits_overlay line 152
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingOverlayWords.rotationWords_vertices line 158