OAI/Combinatorics/KMedianRecovery/Recovery/CoupledResolve.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Outcome line 14
2. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.resolve line 16
3. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Outcome.Correct line 34
4. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.resolve_correct line 38
5. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.banks line 118
6. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.step line 121
7. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.step_correct line 140