OAI/Combinatorics/KMedianRecovery/Recovery/DestinationFacility.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Completion.destinationFacility line 10
2. lemma OAI.MetricKMedianRecovery.Completion.blue_destination_eq line 14
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.destinations_proxy line 24
4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.destinations_uncovered line 28
5. def OAI.MetricKMedianRecovery.Sampling.Comparison.designatedDestination line 32
6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.designatedDestination_mem line 37
7. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.designation_disjoint line 43
8. def OAI.MetricKMedianRecovery.Sampling.Comparison.colorClass line 56
9. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.favorable_destination_green line 59
10. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.favorable_red_rule line 76
11. def OAI.MetricKMedianRecovery.Sampling.Comparison.blueDestination line 94
12. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.blueDestination_uncovered line 98
13. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.blueDestination_mem line 104
14. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.blueDestination_distance line 112