OAI/Combinatorics/KMedian/Projection/CSPProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.PortCSP.Legal line 20
2. def OAI.MetricKMedian.PCP.PortCSP.repair line 23
3. lemma OAI.MetricKMedian.PCP.PortCSP.repair_legal line 26
4. lemma OAI.MetricKMedian.PCP.PortCSP.repair_fixed line 31
5. def OAI.MetricKMedian.PCP.PortCSP.projection line 32
6. lemma OAI.MetricKMedian.PCP.PortCSP.projection_complete line 35
7. lemma OAI.MetricKMedian.PCP.PortCSP.projection_consistent line 43
8. lemma OAI.MetricKMedian.PCP.PortCSP.reject_incidence line 55
9. lemma OAI.MetricKMedian.PCP.PortCSP.projection_sound line 70
10. lemma OAI.MetricKMedian.PCP.PortCSP.projection_expands line 96