OAI/Combinatorics/IndependentSets/Expansion/PoweringPortReindex.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.wordEquiv line 13
2. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.walkEquiv line 19
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.addressEquiv line 22
4. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.labelEquiv line 28
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.wordEnd_map line 40
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.endpoint_map line 48
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.reach_iff line 52
8. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.ballEquiv line 63
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.wordToBall_map line 69
10. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.pullSelector line 75
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 83
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.decode_transport line 89
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 99
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.advanceTail_map line 112
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.edgeAt_map line 120
16. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.pullAccepts line 135
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 138
18. def OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.dartEquiv line 164
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 167
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 180
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 201
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.pullReverse line 218
23. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 224
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 234
25. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 262
26. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 301
27. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 340