OAI/Combinatorics/KMedian/Projection/ToInput.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.BiProjection.indexed line 18
2. lemma OAI.MetricKMedian.PCP.BiProjection.indexed_consistent line 21
3. def OAI.MetricKMedian.PCP.BiProjection.toInput line 22
4. lemma OAI.MetricKMedian.PCP.BiProjection.toInput_perfect line 25
5. lemma OAI.MetricKMedian.PCP.BiProjection.toInput_sound line 28
6. lemma OAI.MetricKMedian.PCP.BiProjection.toInput_u line 31
7. lemma OAI.MetricKMedian.PCP.BiProjection.toInput_v line 33
8. lemma OAI.MetricKMedian.PCP.BiProjection.toInput_degree line 35