OAI/Combinatorics/KMedian/CookLevin/FiniteConstraints.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedian.PCP.FiniteCSP line 12
2. def OAI.MetricKMedian.PCP.FiniteCSP.Satisfies line 19
3. abbrev OAI.MetricKMedian.PCP.FiniteCSP.Label line 20
4. def OAI.MetricKMedian.PCP.FiniteCSP.binary line 21
5. def OAI.MetricKMedian.PCP.FiniteCSP.honest line 26
6. lemma OAI.MetricKMedian.PCP.FiniteCSP.binary_complete line 29
7. def OAI.MetricKMedian.PCP.FiniteCSP.decoded line 33
8. lemma OAI.MetricKMedian.PCP.FiniteCSP.binary_sound line 35
9. lemma OAI.MetricKMedian.PCP.FiniteCSP.binary_iff line 53
10. def OAI.MetricKMedian.PCP.BinaryCSP.pullLabels line 61
11. lemma OAI.MetricKMedian.PCP.BinaryCSP.pullLabels_satisfies line 65
12. lemma OAI.MetricKMedian.PCP.BinaryCSP.pullLabels_complete line 68