OAI/Combinatorics/KMedianRecovery/Branching/CopyAge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalLeaves.level line 10
2. lemma OAI.MetricKMedianRecovery.RationalLeaves.Before.level line 15
3. lemma OAI.MetricKMedianRecovery.RationalLeaves.level_shorten line 21
4. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.level line 35
5. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.before line 40
6. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.Resources.map_bound line 48
7. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.Resources.advance line 53
8. structure OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Output.Resources line 58
9. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Output.Resources.mono line 63
10. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Outcome.Resources line 67