OAI/Combinatorics/IndependentSets/PCP/AlphabetReduction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetReduction.LegalPair line 17
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetReduction.InputCoordinate line 20
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetReduction.pairEncoding line 22
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetReduction.edgeTesterReject line 26
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetReduction.rejected_edge_tester_bound line 30
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetReduction.honest_edge_tester line 46
  7. def OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.restrict line 63
  8. def OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.extend line 67
  9. def OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.canonicalize line 70
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.restrict_apply line 73
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.extend_apply_of_mem line 76
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.extend_apply_of_not_mem line 80
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.restrict_extend line 84
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_mem line 89
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_not_mem line 93
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.restrict_canonicalize line 97
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.canonicalize_idempotent line 101
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.canonicalize_eq_iff line 105
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.expect_restrict line 115
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.expect_canonicalize line 131
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.UniformRestriction.expect_restrict_pair line 136