OAI/Computability/VertexCover/PCP/UniformRestriction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.UniformRestriction.restrict line 13
2. def OAI.UniqueGames.Foundations.PCP.UniformRestriction.extend line 17
3. def OAI.UniqueGames.Foundations.PCP.UniformRestriction.canonicalize line 20
4. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.restrict_apply line 23
5. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.extend_apply_of_mem line 26
6. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.extend_apply_of_not_mem line 30
7. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.restrict_extend line 34
8. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_mem line 39
9. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_not_mem line 43
10. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.restrict_canonicalize line 47
11. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.canonicalize_idempotent line 51
12. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.canonicalize_eq_iff line 55
13. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.expect_restrict line 65
14. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.expect_canonicalize line 81
15. theorem OAI.UniqueGames.Foundations.PCP.UniformRestriction.expect_restrict_pair line 86