OAI/Combinatorics/KMedian/Process/TaperAllProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Taper.ListOperation.AllRaw line 14
2. def OAI.MetricKMedian.Taper.ListOperation.colocated line 16
3. def OAI.MetricKMedian.Taper.ListOperation.extras line 17
4. def OAI.MetricKMedian.Taper.ListOperation.zeroRow line 19
5. def OAI.MetricKMedian.Taper.ListOperation.sourceRow line 21
6. theorem OAI.MetricKMedian.Taper.ListOperation.colocated_poly line 25
7. theorem OAI.MetricKMedian.Taper.ListOperation.extras_poly line 29
8. theorem OAI.MetricKMedian.Taper.ListOperation.zeroRow_poly line 39
9. theorem OAI.MetricKMedian.Taper.ListOperation.sourceRow_poly line 42
10. theorem OAI.MetricKMedian.Taper.ListOperation.colocated_list line 50
11. theorem OAI.MetricKMedian.Taper.ListOperation.extras_list line 53
12. theorem OAI.MetricKMedian.Taper.ListOperation.zeroRow_list line 67
13. theorem OAI.MetricKMedian.Taper.ListOperation.sourceRow_list line 83