OAI/Combinatorics/IndependentSets/Expansion/DegreeReplacement.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.Cloud line 15
2. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.cloudIndexEquiv line 17
3. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.cloudRotation line 27
4. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.cloudRotation_involutive line 32
5. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.innerRotation line 39
6. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.innerRotation_involutive line 43
7. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.innerRotation_tail line 51
8. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacementStep line 57
9. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacementStep_involutive line 64
10. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacementPortGraph line 76
11. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacementGraph line 85
12. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.liftLabel line 101
13. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inl line 104
14. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacement_satisfied_inr line 114
15. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacement_complete line 120
16. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacement_satisfiable line 130
17. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.rejectionCount_eq_sum line 136
18. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.replacement_rejectionCount line 144
19. abbrev OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.PaddedDart line 155
20. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedOwner line 158
21. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedReverse line 163
22. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedReverse_involutive line 167
23. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedGraph line 176
24. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inl line 190
25. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.padded_satisfied_inr line 195
26. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.padded_complete line 199
27. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.padded_satisfiable line 207
28. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.card_paddedDart line 212
29. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.padded_rejectionCount line 218
30. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedReplacementPortGraph line 228
31. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedReplacementGraph line 233
32. theorem OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.paddedReplacement_rejectionCount line 239
33. def OAI.IndependentSetsGames.Foundations.PCP.DegreeReplacement.noDummyEquiv line 248