OAI/Combinatorics/KMedian/Optimization/LPMinimumSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.LPBinary.minimum line 13
  2. theorem OAI.MetricKMedian.LPBinary.minimum_eq_finset line 15
  3. theorem OAI.MetricKMedian.LPBinary.firstNearest_value line 33
  4. theorem OAI.MetricKMedian.LPBinary.firstNearest_le line 38
  5. def OAI.MetricKMedian.LPBinary.selectMinimum line 46
  6. theorem OAI.MetricKMedian.LPBinary.selectMinimum_ofFn line 49
  7. def OAI.MetricKMedian.LPBinary.Program.minFold line 76
  8. def OAI.MetricKMedian.LPBinary.Program.minimumProgram line 83