OAI/Combinatorics/KMedianRecovery/Geometry/NearestMap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.HistoryIsometry.nearest_map line 12
2. lemma OAI.MetricKMedianRecovery.HistoryIsometry.active_map line 26
3. lemma OAI.MetricKMedianRecovery.HistoryIsometry.admissible_map line 32
4. lemma OAI.MetricKMedianRecovery.HistoryIsometry.payment_map line 39
5. lemma OAI.MetricKMedianRecovery.HistoryIsometry.dual_map line 49
6. lemma OAI.MetricKMedianRecovery.HistoryIsometry.openable_map line 59
7. lemma OAI.MetricKMedianRecovery.HistoryIsometry.entry_map line 79
8. lemma OAI.MetricKMedianRecovery.HistoryIsometry.prefix_map line 97
9. lemma OAI.MetricKMedianRecovery.HistoryIsometry.image_union line 109
10. lemma OAI.MetricKMedianRecovery.HistoryIsometry.maximal_map line 116
11. lemma OAI.MetricKMedianRecovery.HistoryIsometry.valid_map line 125
12. theorem OAI.MetricKMedianRecovery.HistoryIsometry.history_map line 134
13. lemma OAI.MetricKMedianRecovery.HistoryIsometry.after_map line 146
14. lemma OAI.MetricKMedianRecovery.HistoryIsometry.paid_map line 155
15. lemma OAI.MetricKMedianRecovery.HistoryIsometry.free_map line 160