OAI/Combinatorics/KMedian/Reduction/ReductionCostProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Reduction.Program.nearestData line 15
2. theorem OAI.MetricKMedian.Reduction.Program.nearestData_poly line 16
3. theorem OAI.MetricKMedian.Reduction.Program.nearestData_view line 19
4. def OAI.MetricKMedian.Reduction.Program.costData line 31
5. theorem OAI.MetricKMedian.Reduction.Program.costData_poly line 33
6. theorem OAI.MetricKMedian.Reduction.Program.costData_view line 37
7. def OAI.MetricKMedian.Reduction.Program.diff line 45
8. def OAI.MetricKMedian.Reduction.Program.union line 46
9. theorem OAI.MetricKMedian.Reduction.Program.diff_poly line 47
10. theorem OAI.MetricKMedian.Reduction.Program.union_poly line 48
11. theorem OAI.MetricKMedian.Reduction.Program.diff_view line 49
12. theorem OAI.MetricKMedian.Reduction.Program.union_view line 51