OAI/Combinatorics/KMedian/Projection/RegularTable.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.edgeSource line 14
2. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_edgeSource line 17
3. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.edgeProject line 21
4. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_edgeProject line 23
5. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.edgeRow line 27
6. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_edgeRow line 30
7. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.regularTable line 36
8. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_regularTable line 39
9. abbrev OAI.MetricKMedian.PCP.Compiler.SeedProgram.nodeEquiv line 46
10. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.nodeOrder line 47
11. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.rootEquiv line 49
12. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.projection line 50
13. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.edgeSource_correct line 53
14. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.edgeRow_correct line 62
15. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.regularTable_build line 71