OAI/Combinatorics/KMedianRecovery/Strictness/SortedDual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.SortedIndex.equiv_dual line 10
2. lemma OAI.MetricKMedianRecovery.SortedIndex.equiv_dual_val line 11
3. lemma OAI.MetricKMedianRecovery.SortedIndex.enum_symm line 12
4. lemma OAI.MetricKMedianRecovery.SortedIndex.image_enum line 14
5. lemma OAI.MetricKMedianRecovery.SortedIndex.sum_enum_dual line 22
6. lemma OAI.MetricKMedianRecovery.SortedIndex.sum_cost line 27
7. lemma OAI.MetricKMedianRecovery.SortedIndex.dual_on_points line 29
8. lemma OAI.MetricKMedianRecovery.SortedIndex.sum_budget line 61