OAI/Combinatorics/KMedianRecovery/Machines/MergeResources.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalLeaves.HeightBound line 10
2. lemma OAI.MetricKMedianRecovery.RationalLeaves.parent_shorten line 14
3. lemma OAI.MetricKMedianRecovery.RationalLeaves.height_shorten line 22
4. structure OAI.MetricKMedianRecovery.RationalLeaves.BankBound line 31
5. lemma OAI.MetricKMedianRecovery.RationalLeaves.BankBound.mono line 38
6. lemma OAI.MetricKMedianRecovery.RationalLeaves.BankBound.pool line 43
7. lemma OAI.MetricKMedianRecovery.RationalLeaves.BankBound.insert line 66
8. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.Bounded line 86
9. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.parent line 90
10. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.height line 95
11. structure OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.Resources line 101
12. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.State.Resources.map_bank line 107