OAI/Combinatorics/IndependentSets/PCP/AlphabetRetraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.pullback line 11
2. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.edgeSatisfied_pullback line 18
3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.rejectionCount_pullback line 23
4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.satisfiable_pullback_iff line 28
5. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.Label64 line 40
6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.decode64 line 42
7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.encode64 line 44
8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.decode_encode64 line 47
9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.initial64 line 52
10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.initial64_satisfiable_iff line 56
11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.initial64_alphabet line 61
12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetRetraction.initial64_inverse_size_gap line 64