OAI/Combinatorics/IndependentSets/PCP/AmplificationRound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.Label line 10
2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.Addresses line 11
3. abbrev OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.PoweredAlphabet line 12
4. instance OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.(instance at line 15) line 15
5. instance OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.(instance at line 16) line 16
6. abbrev OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.PoweredDart line 21
7. instance OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.(instance at line 25) line 25
8. def OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.selectors line 27
9. def OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.powered line 34
10. abbrev OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.Vertex line 40
11. abbrev OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.Dart line 45
12. instance OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.(instance at line 48) line 48
13. instance OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.(instance at line 57) line 57
14. instance OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.(instance at line 60) line 60
15. def OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.graph line 62
16. theorem OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.powered_completeness line 67
17. theorem OAI.IndependentSetsGames.Foundations.PCP.AmplificationRound.completeness line 80