OAI/Combinatorics/KMedianRecovery/Recovery/Data.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedianRecovery.PhaseLeafGeometry.Data line 11
2. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.empty line 22
3. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.mapRoot line 25
4. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.mapLength line 28
5. lemma OAI.MetricKMedianRecovery.PhaseLeafGeometry.mapRoot_apply line 33
6. lemma OAI.MetricKMedianRecovery.PhaseLeafGeometry.mapLength_apply line 39
7. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.Data.map line 45
8. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.Data.attach line 75