OAI/Combinatorics/KMedianRecovery/Algorithms/ExtendBudget.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedianRecovery.extendBudgetline 9 - lemma
OAI.MetricKMedianRecovery.extendBudget_atline 12 - lemma
OAI.MetricKMedianRecovery.sum_liftSubsetline 15 - theorem
OAI.MetricKMedianRecovery.execution_dual_on_pointsline 26 - theorem
OAI.MetricKMedianRecovery.execution_strict_on_pointsline 42