OAI/Combinatorics/IndependentSets/Expansion/PoweringLabels.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.PortWords line 13
2. instance OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.finitePortWords line 15
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.Ball line 19
4. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.wordToBall line 22
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.wordToBall_surjective line 25
6. instance OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.finiteBall line 32
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.card_portWords line 36
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.card_ball_le line 40
9. structure OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.AddressSelector line 47
10. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.classicalSelector line 51
11. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.scanWitness line 56
12. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.listSelector line 67
13. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.PaddedLabel line 78
14. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.encode line 80
15. def OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.decode line 83
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.decode_encode line 86
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.decode_surjective line 93
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.encode_injective line 97
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.decoded_word_collision line 104
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringLabels.card_paddedLabel line 110
21. def OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.allWords line 123
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.mem_allWords line 128
23. def OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.allAddresses line 144
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.mem_allAddresses line 148
25. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.length_allWords line 156
26. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.length_allAddresses line 166
27. def OAI.IndependentSetsGames.Foundations.PCP.PoweringAddresses.finitePortSelector line 172