OAI/Combinatorics/KMedian/CookLevin/TM2Response.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Tableau.BoundedList line 12
2. def OAI.MetricKMedian.PCP.Tableau.BoundedList.cells line 15
3. lemma OAI.MetricKMedian.PCP.Tableau.BoundedList.cells_injective line 16
4. instance OAI.MetricKMedian.PCP.Tableau.BoundedList.(instance at line 25) line 25
5. def OAI.MetricKMedian.PCP.Tableau.radius line 32
6. lemma OAI.MetricKMedian.PCP.Tableau.depth_le line 34
7. def OAI.MetricKMedian.PCP.Tableau.advance line 37
8. abbrev OAI.MetricKMedian.PCP.Tableau.Control line 42
9. abbrev OAI.MetricKMedian.PCP.Tableau.Prefix line 43
10. abbrev OAI.MetricKMedian.PCP.Tableau.Response line 44
11. def OAI.MetricKMedian.PCP.Tableau.respond line 45
12. def OAI.MetricKMedian.PCP.Tableau.stackPrefix line 55
13. lemma OAI.MetricKMedian.PCP.Tableau.advance_stackPrefix line 57
14. lemma OAI.MetricKMedian.PCP.Tableau.response_control line 71
15. lemma OAI.MetricKMedian.PCP.Tableau.response_stack line 75
16. lemma OAI.MetricKMedian.PCP.Tableau.response_cell line 81
17. lemma OAI.MetricKMedian.PCP.Tableau.advance_length line 91