OAI/Combinatorics/KMedianRecovery/Geometry/FamilyMetric.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.FreshCopyEndpoints.familyMetric line 13
2. def OAI.MetricKMedianRecovery.FreshCopyEndpoints.incl line 17
3. lemma OAI.MetricKMedianRecovery.FreshCopyEndpoints.original_dist line 20
4. lemma OAI.MetricKMedianRecovery.FreshCopyEndpoints.leaf_dist line 26
5. lemma OAI.MetricKMedianRecovery.FreshCopyEndpoints.fresh line 32
6. theorem OAI.MetricKMedianRecovery.FreshCopyEndpoints.zero_endpoint line 35
7. lemma OAI.MetricKMedianRecovery.FreshCopyEndpoints.live_map line 86
8. theorem OAI.MetricKMedianRecovery.FreshCopyEndpoints.disabling_endpoint line 102