OAI/Combinatorics/KMedianRecovery/Geometry/Metric.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalMetricInput.metric line 9
2. lemma OAI.MetricKMedianRecovery.RationalMetricInput.cast_inf' line 15
3. lemma OAI.MetricKMedianRecovery.RationalMetricInput.metric_cost line 23
4. lemma OAI.MetricKMedianRecovery.RationalMetricInput.metric_optimum line 33
5. lemma OAI.MetricKMedianRecovery.RationalMetricInput.cost_nonneg line 42
6. lemma OAI.MetricKMedianRecovery.RationalMetricInput.optimum_nonneg line 47
7. def OAI.MetricKMedianRecovery.RationalMetricInput.outputBits line 52
8. lemma OAI.MetricKMedianRecovery.RationalMetricInput.decode_outputBits line 55