OAI/Combinatorics/KMedianRecovery/Geometry/NearestInsertEqual.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.CoincidentCopy.nearest_insert_equal line 9
2. lemma OAI.MetricKMedianRecovery.CoincidentCopy.active_insert_equal line 21
3. lemma OAI.MetricKMedianRecovery.CoincidentCopy.clipped_insert_equal line 26
4. lemma OAI.MetricKMedianRecovery.CoincidentCopy.admissible_insert_equal line 31
5. lemma OAI.MetricKMedianRecovery.CoincidentCopy.payment_insert_equal line 40
6. lemma OAI.MetricKMedianRecovery.CoincidentCopy.dual_insert_equal line 47
7. theorem OAI.MetricKMedianRecovery.CoincidentCopy.openable_insert_equal line 53
8. lemma OAI.MetricKMedianRecovery.CoincidentCopy.payment_zero line 63
9. lemma OAI.MetricKMedianRecovery.CoincidentCopy.not_openable line 84
10. theorem OAI.MetricKMedianRecovery.CoincidentCopy.maximal_replace line 92
11. lemma OAI.MetricKMedianRecovery.CoincidentCopy.paid_count line 111