OAI/Combinatorics/KMedianRecovery/Recovery/Virtual.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MetricKMedianRecovery.Completion.Virtual line 10
  2. def OAI.MetricKMedianRecovery.Completion.virtualDistance line 16
  3. def OAI.MetricKMedianRecovery.Completion.withGhosts line 22
  4. lemma OAI.MetricKMedianRecovery.Completion.withGhosts_nonempty line 26
  5. lemma OAI.MetricKMedianRecovery.Completion.real_mem_withGhosts line 30
  6. lemma OAI.MetricKMedianRecovery.Completion.ball_mem_withGhosts line 34
  7. lemma OAI.MetricKMedianRecovery.Completion.permanent_mem_withGhosts line 38
  8. def OAI.MetricKMedianRecovery.Completion.virtualNearest line 41
  9. def OAI.MetricKMedianRecovery.Completion.nearestTag line 45
  10. lemma OAI.MetricKMedianRecovery.Completion.nearestTag_mem line 50
  11. lemma OAI.MetricKMedianRecovery.Completion.nearestTag_distance line 56
  12. lemma OAI.MetricKMedianRecovery.Completion.virtualNearest_nonneg line 66
  13. def OAI.MetricKMedianRecovery.Completion.distanceTo line 76
  14. lemma OAI.MetricKMedianRecovery.Completion.distanceTo_nonneg line 80
  15. lemma OAI.MetricKMedianRecovery.Completion.distanceTo_le line 84
  16. lemma OAI.MetricKMedianRecovery.Completion.distanceTo_triangle line 88
  17. lemma OAI.MetricKMedianRecovery.Completion.cappedCost_nonneg line 95
  18. lemma OAI.MetricKMedianRecovery.Completion.le_cappedCost line 99
  19. lemma OAI.MetricKMedianRecovery.Completion.completion_cardinality line 105
  20. def OAI.MetricKMedianRecovery.Completion.assignmentWeight line 126
  21. lemma OAI.MetricKMedianRecovery.Completion.assignmentWeight_nonneg line 131
  22. lemma OAI.MetricKMedianRecovery.Completion.assignmentWeight_sum line 136