OAI/Computability/VertexCover/PCP/AlphabetGraphBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 12
2. abbrev OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.OutputDart line 15
3. def OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 17
4. def OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 20
5. def OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.dartFactor line 22
6. def OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 24
7. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 26
8. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 33
9. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 71
10. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 81
11. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.card_output_total line 88
12. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 97
13. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 115
14. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 121