OAI/Combinatorics/KMedianRecovery/Recovery/Finished.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.PhaseGeometricMerge.Finished line 13
2. def OAI.MetricKMedianRecovery.PhaseGeometricMerge.Solved line 17
3. lemma OAI.MetricKMedianRecovery.PhaseGeometricMerge.Solved.of_finished line 24
4. lemma OAI.MetricKMedianRecovery.PhaseGeometricMerge.Solved.pullback line 33
5. lemma OAI.MetricKMedianRecovery.PhaseGeometricMerge.finish line 48
6. structure OAI.MetricKMedianRecovery.PhaseGeometricMerge.Coupled line 61
7. def OAI.MetricKMedianRecovery.PhaseGeometricMerge.same line 66
8. theorem OAI.MetricKMedianRecovery.PhaseGeometricMerge.advance line 77