OAI/Combinatorics/KMedianRecovery/Recovery/ActiveInsert.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.DisablingCopy.active_insert line 9
  2. lemma OAI.MetricKMedianRecovery.DisablingCopy.inactive_distance line 15
  3. lemma OAI.MetricKMedianRecovery.DisablingCopy.budgets_insert line 31
  4. lemma OAI.MetricKMedianRecovery.DisablingCopy.admissible_insert line 42
  5. lemma OAI.MetricKMedianRecovery.DisablingCopy.payment_insert line 63
  6. lemma OAI.MetricKMedianRecovery.DisablingCopy.dual_insert line 76
  7. theorem OAI.MetricKMedianRecovery.DisablingCopy.openable_insert line 82
  8. lemma OAI.MetricKMedianRecovery.DisablingCopy.numerical_bound line 93
  9. lemma OAI.MetricKMedianRecovery.DisablingHistory.member_ne line 112
  10. theorem OAI.MetricKMedianRecovery.DisablingHistory.entry_insert line 116
  11. theorem OAI.MetricKMedianRecovery.DisablingHistory.prefix_insert line 139
  12. theorem OAI.MetricKMedianRecovery.DisablingHistory.valid_insert line 150
  13. theorem OAI.MetricKMedianRecovery.DisablingHistory.history_insert line 166
  14. lemma OAI.MetricKMedianRecovery.DisablingHistory.after_insert line 184
  15. theorem OAI.MetricKMedianRecovery.DisablingHistory.prepend_disabled_copy line 192