OAI/Combinatorics/KMedian/Projection/Input.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedian.PCP.BiProjection.systemline 17 - lemma
OAI.MetricKMedian.PCP.BiProjection.system_regularline 21 - lemma
OAI.MetricKMedian.PCP.BiProjection.system_consistentline 32 - def
OAI.MetricKMedian.PCP.BiProjection.inputline 47 - lemma
OAI.MetricKMedian.PCP.BiProjection.input_perfectline 61 - lemma
OAI.MetricKMedian.PCP.BiProjection.system_scoreline 73 - lemma
OAI.MetricKMedian.PCP.BiProjection.input_soundline 89