OAI/Combinatorics/KMedianRecovery/Recovery/CoupledFinish.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.finish line 12
2. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.finish_correct line 15
3. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.sameState line 27
4. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.same_certified line 30
5. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.Runs.cons_iff line 73
6. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.aligned_phase line 99
7. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.advanceState line 116
8. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.advance_certified line 119