OAI/Combinatorics/KMedian/CookLevin/TM2Locality.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Tableau.depth line 13
2. def OAI.MetricKMedian.PCP.Tableau.Safe line 22
3. def OAI.MetricKMedian.PCP.Tableau.appendCfg line 24
4. lemma OAI.MetricKMedian.PCP.Tableau.append_update line 27
5. lemma OAI.MetricKMedian.PCP.Tableau.safe_mono line 34
6. lemma OAI.MetricKMedian.PCP.Tableau.safe_update line 36
7. lemma OAI.MetricKMedian.PCP.Tableau.head_append line 43
8. lemma OAI.MetricKMedian.PCP.Tableau.tail_append line 49
9. lemma OAI.MetricKMedian.PCP.Tableau.stepAux_suffix line 55
10. lemma OAI.MetricKMedian.PCP.Tableau.take_drop_safe line 90
11. lemma OAI.MetricKMedian.PCP.Tableau.stepAux_prefix line 96
12. lemma OAI.MetricKMedian.PCP.Tableau.stepAux_length line 104