OAI/Combinatorics/KMedianRecovery/Geometry/NearestImage.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.CoincidentHistory.nearest_image line 12
  2. lemma OAI.MetricKMedianRecovery.CoincidentHistory.active_image line 24
  3. lemma OAI.MetricKMedianRecovery.CoincidentHistory.admissible_image line 30
  4. lemma OAI.MetricKMedianRecovery.CoincidentHistory.payment_image line 35
  5. lemma OAI.MetricKMedianRecovery.CoincidentHistory.dual_image line 43
  6. lemma OAI.MetricKMedianRecovery.CoincidentHistory.openable_image line 51
  7. lemma OAI.MetricKMedianRecovery.CoincidentHistory.swap_distances line 58
  8. lemma OAI.MetricKMedianRecovery.CoincidentHistory.swap_alphabet line 68
  9. theorem OAI.MetricKMedianRecovery.CoincidentHistory.entry_swap line 78
  10. theorem OAI.MetricKMedianRecovery.CoincidentHistory.prefix_swap line 104
  11. theorem OAI.MetricKMedianRecovery.CoincidentHistory.maximal_swap line 115
  12. theorem OAI.MetricKMedianRecovery.CoincidentHistory.valid_swap line 138
  13. theorem OAI.MetricKMedianRecovery.CoincidentHistory.history_swap line 147
  14. lemma OAI.MetricKMedianRecovery.CoincidentHistory.swap_set line 160
  15. lemma OAI.MetricKMedianRecovery.CoincidentHistory.paid_swap line 176
  16. lemma OAI.MetricKMedianRecovery.CoincidentHistory.free_swap line 185
  17. lemma OAI.MetricKMedianRecovery.CoincidentHistory.phase_free_swap line 195
  18. theorem OAI.MetricKMedianRecovery.CoincidentHistory.endpoint line 211