OAI/Combinatorics/KMedianRecovery/Recovery/Mono.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.PhaseSequence.Entry.mono line 11
2. lemma OAI.MetricKMedianRecovery.PhaseSequence.Entry.mem line 17
3. lemma OAI.MetricKMedianRecovery.PhaseSequence.Prefix.mono line 25
4. lemma OAI.MetricKMedianRecovery.PhaseSequence.Prefix.sublist line 31
5. lemma OAI.MetricKMedianRecovery.PhaseSequence.Prefix.append line 42
6. lemma OAI.MetricKMedianRecovery.PhaseSequence.Prefix.opened_subset line 52
7. lemma OAI.MetricKMedianRecovery.PhaseSequence.Prefix.disjoint line 62
8. lemma OAI.MetricKMedianRecovery.PhaseSequence.Prefix.nodup line 69
9. lemma OAI.MetricKMedianRecovery.PhaseSequence.exact_opening_eta line 81
10. theorem OAI.MetricKMedianRecovery.PhaseSequence.complete line 90
11. theorem OAI.MetricKMedianRecovery.PhaseSequence.complete_after line 121