OAI/Combinatorics/KMedian/CookLevin/CookBox.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MetricKMedian.PCP.CookLevin.valueInhabited line 20
2. abbrev OAI.MetricKMedian.PCP.CookLevin.Variable line 22
3. abbrev OAI.MetricKMedian.PCP.CookLevin.Test line 23
4. abbrev OAI.MetricKMedian.PCP.CookLevin.Alphabet line 24
5. instance OAI.MetricKMedian.PCP.CookLevin.testNonempty line 25
6. def OAI.MetricKMedian.PCP.CookLevin.box line 27
7. lemma OAI.MetricKMedian.PCP.CookLevin.box_correct line 29