OAI/Combinatorics/KMedian/Geometry/RationalInstanceCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.rationalNearest line 12
2. def OAI.MetricKMedian.rationalCost line 17
3. theorem OAI.MetricKMedian.Instance.cast_rationalNearest line 22
4. theorem OAI.MetricKMedian.Instance.cast_rationalCost line 36
5. theorem OAI.MetricKMedian.Instance.nearest_antitone line 40
6. theorem OAI.MetricKMedian.Instance.cost_antitone line 47
7. theorem OAI.MetricKMedian.Instance.rationalCost_antitone line 51
8. theorem OAI.MetricKMedian.Instance.deletion_cost_nonneg line 57