OAI/Combinatorics/KMedianRecovery/Recovery/SubsetSubtypeRepresentative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Completion.subset_subtype_representative line 10
2. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.nonproxy_remaining_in line 30
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.favorable_color_subsets line 36
4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.affordable_blue_destinations line 52
5. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.favorable_computedPlan line 64
6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.favorable_counter_bound line 106