OAI/Combinatorics/KMedianRecovery/Recovery/CountedTrace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MetricKMedianRecovery.CountedTrace line 8
2. lemma OAI.MetricKMedianRecovery.CountedTrace.append line 15
3. lemma OAI.MetricKMedianRecovery.CountedTrace.map line 20
4. lemma OAI.MetricKMedianRecovery.CountedTrace.invariant line 24
5. lemma OAI.MetricKMedianRecovery.CountedTrace.exists_path line 29
6. def OAI.MetricKMedianRecovery.OrdinaryProducer.PlainOpening line 46
7. def OAI.MetricKMedianRecovery.OrdinaryProducer.PhaseMaximal line 55
8. lemma OAI.MetricKMedianRecovery.OrdinaryProducer.PlainOpening.atomic line 60
9. lemma OAI.MetricKMedianRecovery.OrdinaryProducer.PlainOpening.phase_eq line 63
10. lemma OAI.MetricKMedianRecovery.OrdinaryProducer.PlainOpening.opened_in line 66
11. lemma OAI.MetricKMedianRecovery.OrdinaryProducer.PlainOpening.remaining_drop line 69
12. theorem OAI.MetricKMedianRecovery.OrdinaryProducer.complete_phase line 78