OAI/Combinatorics/KMedian/Reduction/ReductionClosure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.selectFeasible line 13
  2. theorem OAI.MetricKMedian.Reduction.selectFeasible_spec line 17
  3. def OAI.MetricKMedian.Reduction.zeroSet line 41
  4. theorem OAI.MetricKMedian.Reduction.zeroSet_spec line 44
  5. theorem OAI.MetricKMedian.Reduction.reduction_parameters line 61
  6. def OAI.MetricKMedian.Reduction.ordinaryReduction line 86
  7. theorem OAI.MetricKMedian.Reduction.ordinaryReduction_spec line 91
  8. theorem OAI.MetricKMedian.Reduction.ordinaryReduction_parameters line 116