OAI/Combinatorics/KMedianRecovery/Recovery/SmallSubsets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.LocalSearch.smallSubsets line 9
2. lemma OAI.MetricKMedianRecovery.LocalSearch.mem_smallSubsets line 11
3. lemma OAI.MetricKMedianRecovery.LocalSearch.smallSubsets_card line 20
4. def OAI.MetricKMedianRecovery.LocalSearch.exchangeCandidates line 34
5. lemma OAI.MetricKMedianRecovery.LocalSearch.candidate_mem_self line 38
6. lemma OAI.MetricKMedianRecovery.LocalSearch.candidate_properties line 44
7. lemma OAI.MetricKMedianRecovery.LocalSearch.candidate_of_exchange line 56
8. lemma OAI.MetricKMedianRecovery.LocalSearch.exchangeCandidates_card line 67
9. def OAI.MetricKMedianRecovery.LocalSearch.descentStep line 82
10. lemma OAI.MetricKMedianRecovery.LocalSearch.descentStep_mem line 85
11. lemma OAI.MetricKMedianRecovery.LocalSearch.descentStep_min line 89
12. theorem OAI.MetricKMedianRecovery.LocalSearch.bounded_descent line 94