OAI/Combinatorics/KMedian/Reduction/LocalCompletion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.CloseCenters.region line 18
  2. def OAI.MetricKMedian.Reduction.CloseCenters.matched line 21
  3. def OAI.MetricKMedian.Reduction.CloseCenters.backup line 24
  4. theorem OAI.MetricKMedian.Reduction.CloseCenters.matched_sub line 27
  5. theorem OAI.MetricKMedian.Reduction.CloseCenters.optimal_mem line 32
  6. theorem OAI.MetricKMedian.Reduction.CloseCenters.region_disjoint line 40
  7. theorem OAI.MetricKMedian.Reduction.CloseCenters.region_reference line 46
  8. theorem OAI.MetricKMedian.Reduction.CloseCenters.choose_local line 56