OAI/Combinatorics/KMedian/Projection/Promises.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedian.PCP.BiProjection.perfect_prodline 15 - lemma
OAI.MetricKMedian.PCP.BiProjection.consistent_prodline 21 - lemma
OAI.MetricKMedian.PCP.BiProjection.perfect_powerline 26 - lemma
OAI.MetricKMedian.PCP.BiProjection.consistent_powerline 30