OAI/Combinatorics/KMedianRecovery/Recovery/BallSet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Completion.ballSet line 8
  2. abbrev OAI.MetricKMedianRecovery.Completion.CopiedBall line 12
  3. def OAI.MetricKMedianRecovery.Completion.copiedPart line 14
  4. def OAI.MetricKMedianRecovery.Completion.copiedLoc line 16
  5. lemma OAI.MetricKMedianRecovery.Completion.copiedLoc_mem line 18
  6. lemma OAI.MetricKMedianRecovery.Completion.copiedLoc_distance line 21
  7. lemma OAI.MetricKMedianRecovery.Completion.copiedPart_surjective line 26
  8. lemma OAI.MetricKMedianRecovery.Completion.copiedBall_card_le line 32
  9. lemma OAI.MetricKMedianRecovery.Completion.copied_comparison line 44