OAI/Combinatorics/KMedian/Rounding/RationalRetain.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.RationalRetain.keep line 10
2. theorem OAI.MetricKMedian.RationalRetain.le line 14
3. theorem OAI.MetricKMedian.RationalRetain.zero line 23
4. theorem OAI.MetricKMedian.RationalRetain.total line 26
5. def OAI.MetricKMedian.RationalRetain.retained line 36
6. theorem OAI.MetricKMedian.RationalRetain.retained_le line 39
7. theorem OAI.MetricKMedian.RationalRetain.retained_total line 42