OAI/Computability/VertexCover/PCP/ConstraintGraph.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGames.Foundations.PCP.ConstraintGraph line 10
2. def OAI.UniqueGames.Foundations.PCP.ConstraintGraph.head line 21
3. theorem OAI.UniqueGames.Foundations.PCP.ConstraintGraph.head_reverse line 23
4. def OAI.UniqueGames.Foundations.PCP.ConstraintGraph.edgeSatisfied line 27
5. theorem OAI.UniqueGames.Foundations.PCP.ConstraintGraph.edgeSatisfied_reverse line 30
6. def OAI.UniqueGames.Foundations.PCP.ConstraintGraph.Satisfiable line 36
7. def OAI.UniqueGames.Foundations.PCP.ConstraintGraph.rejectedDarts line 39
8. def OAI.UniqueGames.Foundations.PCP.ConstraintGraph.rejectionCount line 42
9. theorem OAI.UniqueGames.Foundations.PCP.ConstraintGraph.mem_rejectedDarts line 45
10. theorem OAI.UniqueGames.Foundations.PCP.ConstraintGraph.rejectionCount_le line 50
11. theorem OAI.UniqueGames.Foundations.PCP.ConstraintGraph.rejected_exists_of_not_satisfiable line 54
12. theorem OAI.UniqueGames.Foundations.PCP.ConstraintGraph.rejectionCount_positive line 66