OAI/Combinatorics/KMedian/CookLevin/TableauLocal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Tableau.Tops line 17
2. def OAI.MetricKMedian.PCP.Tableau.PrefixRelation line 18
3. lemma OAI.MetricKMedian.PCP.Tableau.prefixRelation_exact line 20
4. lemma OAI.MetricKMedian.PCP.Tableau.prefixRelation_complete line 31
5. def OAI.MetricKMedian.PCP.Tableau.category line 39
6. def OAI.MetricKMedian.PCP.Tableau.cellTable line 40
7. lemma OAI.MetricKMedian.PCP.Tableau.cellTable_exact line 43
8. def OAI.MetricKMedian.PCP.Tableau.clampedCell line 61
9. lemma OAI.MetricKMedian.PCP.Tableau.clampedCell_eq line 64
10. lemma OAI.MetricKMedian.PCP.Tableau.local_transition_exact line 72