OAI/Combinatorics/KMedianRecovery/Recovery/RealFilling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Completion.exists_real_filling line 9
2. lemma OAI.MetricKMedianRecovery.Completion.padded_completion line 43
3. lemma OAI.MetricKMedianRecovery.Completion.virtual_domination line 57
4. lemma OAI.MetricKMedianRecovery.Completion.nearest_le_virtualNearest line 74
5. lemma OAI.MetricKMedianRecovery.Completion.nearest_le_redCost line 83
6. lemma OAI.MetricKMedianRecovery.Completion.sum_assignment_charges line 96