OAI/Combinatorics/KMedian/Reduction/BudgetReduction.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedian.Instance.restrictFacilitiesline 14 - theorem
OAI.MetricKMedian.Instance.restrict_costline 17 - theorem
OAI.MetricKMedian.Instance.padded_optimumline 20 - theorem
OAI.MetricKMedian.Instance.restrict_optimumline 28 - def
OAI.MetricKMedian.Reduction.reductionOutputsline 41 - theorem
OAI.MetricKMedian.Reduction.reductionOutputs_successline 47 - theorem
OAI.MetricKMedian.Reduction.reductionOutputs_cardline 80