OAI/Combinatorics/KMedian/Reduction/CompletionEnumeration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.rationalRadii line 15
  2. def OAI.MetricKMedian.Reduction.completionBranches line 18
  3. theorem OAI.MetricKMedian.Reduction.completionBranches_card line 23
  4. theorem OAI.MetricKMedian.Reduction.Serving.radius_rational line 38
  5. def OAI.MetricKMedian.Reduction.Serving.badSet line 50
  6. theorem OAI.MetricKMedian.Reduction.Serving.badSet_sub line 53
  7. theorem OAI.MetricKMedian.Reduction.Serving.badSet_card line 58
  8. theorem OAI.MetricKMedian.Reduction.Serving.sdiff_badSet line 61
  9. theorem OAI.MetricKMedian.Reduction.completion_branch_exists line 80