OAI/Combinatorics/KMedian/CookLevin/TableauEndpoints.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedian.PCP.Tableau.bounded_soundline 18 - lemma
OAI.MetricKMedian.PCP.Tableau.bounded_completeline 29 - lemma
OAI.MetricKMedian.PCP.Tableau.path_completeline 55