OAI/Combinatorics/KMedianRecovery/Recovery/Produce.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedianRecovery.PhaseSurplusProducer.produce line 10
2. def OAI.MetricKMedianRecovery.LocalSearch.feasibleSets line 97
3. lemma OAI.MetricKMedianRecovery.LocalSearch.mem_feasibleSets line 100
4. lemma OAI.MetricKMedianRecovery.LocalSearch.feasibleSets_nonempty line 104
5. def OAI.MetricKMedianRecovery.LocalSearch.optimum line 109
6. lemma OAI.MetricKMedianRecovery.LocalSearch.optimum_nonneg line 111
7. lemma OAI.MetricKMedianRecovery.LocalSearch.optimum_le line 116
8. lemma OAI.MetricKMedianRecovery.LocalSearch.optimum_attained line 121
9. lemma OAI.MetricKMedianRecovery.LocalSearch.optimum_attained_exact line 129
10. lemma OAI.MetricKMedianRecovery.LocalSearch.optimum_antitone line 137