OAI/Combinatorics/KMedian/CookLevin/TableauRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.Tableau.blank_propagates line 12
2. lemma OAI.MetricKMedian.PCP.Tableau.row_list line 19
3. abbrev OAI.MetricKMedian.PCP.Tableau.Row line 43
4. def OAI.MetricKMedian.PCP.Tableau.rowCell line 44
5. def OAI.MetricKMedian.PCP.Tableau.ValidRow line 46
6. lemma OAI.MetricKMedian.PCP.Tableau.valid_row_list line 49
7. def OAI.MetricKMedian.PCP.Tableau.listRow line 62
8. lemma OAI.MetricKMedian.PCP.Tableau.listRow_valid line 63
9. lemma OAI.MetricKMedian.PCP.Tableau.listRow_cell line 71
10. lemma OAI.MetricKMedian.PCP.Tableau.list_eq_of_row line 78
11. lemma OAI.MetricKMedian.PCP.Tableau.stack_eq_of_cells line 86