OAI/Combinatorics/KMedian/Machines/Box.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedian.PCP.Amplifier.Box line 12
2. instance OAI.MetricKMedian.PCP.Amplifier.Box.edgeNonempty line 19
3. def OAI.MetricKMedian.PCP.Amplifier.Box.Perfect line 20
4. def OAI.MetricKMedian.PCP.Amplifier.Box.Rejects line 21
5. def OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP line 23
6. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_complete line 28
7. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_sound line 31
8. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_iff line 37
9. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_nodes line 42
10. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_edges line 43
11. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_edges_le line 44
12. lemma OAI.MetricKMedian.PCP.Amplifier.Box.ofCSP_size_le line 46