OAI/Computability/VertexCover/PCP/LazyConstraint.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.LazyConstraint.constraintGraph line 16
2. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.constraintGraph_tail line 28
3. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 31
4. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 34
5. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 38
6. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 42
7. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.complete line 51
8. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.complete_iff line 61
9. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.satisfiable_iff line 72
10. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.rejectionCount_eq line 80
11. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.card_ports line 89
12. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.card_darts line 93
13. theorem OAI.UniqueGames.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 97