OAI/Combinatorics/KMedian/Instance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Instance.pseudoMetric line 13
2. theorem OAI.MetricKMedian.Instance.facilities_nonempty line 19
3. theorem OAI.MetricKMedian.Instance.feasible_nonempty line 22
4. theorem OAI.MetricKMedian.Instance.mem_feasible line 28
5. theorem OAI.MetricKMedian.Instance.nearest_nonneg line 32
6. theorem OAI.MetricKMedian.Instance.nearest_le line 42
7. theorem OAI.MetricKMedian.Instance.nearest_attained line 47
8. theorem OAI.MetricKMedian.Instance.cost_nonneg line 53
9. theorem OAI.MetricKMedian.Instance.cost_le_assignment line 56
10. theorem OAI.MetricKMedian.Instance.optimum_attained line 62
11. theorem OAI.MetricKMedian.Instance.optimum_nonneg line 70
12. theorem OAI.MetricKMedian.Instance.optimum_le line 75
13. theorem OAI.MetricKMedian.Instance.cost_eq_zero_iff line 80
14. theorem OAI.MetricKMedian.Instance.optimum_eq_zero_iff line 96