OAI/Combinatorics/KMedianRecovery/Recovery/FinishSpec.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedianRecovery.RationalPhase.finish_spec line 9
2. theorem OAI.MetricKMedianRecovery.RationalPhase.complete_spec line 48
3. inductive OAI.MetricKMedianRecovery.OrdinaryProducer.OrdinaryStep line 68
4. lemma OAI.MetricKMedianRecovery.OrdinaryProducer.OrdinaryStep.atomic line 76
5. lemma OAI.MetricKMedianRecovery.OrdinaryProducer.OrdinaryStep.opened_in line 80