OAI/Combinatorics/IndependentSets/PCP/AlphabetGraphBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 10
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.OutputDart line 13
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 15
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 18
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.dartFactor line 20
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 22
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 24
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 31
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 70
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 79
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.card_output_total line 85
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 92
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 109
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 114
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.gap_transfer_real line 127
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.build_vertices line 155
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.build_darts line 165
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.build_total line 173
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.build_total_le line 180
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.build_vertices_le line 197
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.build_darts_le line 202
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTableBounds.sizeFactor_positive line 207