OAI/Combinatorics/KMedian/Optimization/TruncatedListOperations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.LPBinary.range_ofFn line 14
  2. def OAI.MetricKMedian.LPBinary.Truncated.row line 21
  3. def OAI.MetricKMedian.LPBinary.Truncated.matrix line 22
  4. def OAI.MetricKMedian.LPBinary.Truncated.objective line 23
  5. def OAI.MetricKMedian.LPBinary.Truncated.component line 25
  6. def OAI.MetricKMedian.LPBinary.Truncated.gradient line 28
  7. def OAI.MetricKMedian.LPBinary.Truncated.next line 31
  8. theorem OAI.MetricKMedian.LPBinary.Truncated.row_ofFn line 34
  9. theorem OAI.MetricKMedian.LPBinary.Truncated.matrix_ofFn line 38
  10. theorem OAI.MetricKMedian.LPBinary.Truncated.objective_ofFn line 44
  11. theorem OAI.MetricKMedian.LPBinary.Truncated.component_ofFn line 50
  12. theorem OAI.MetricKMedian.LPBinary.Truncated.gradient_ofFn line 56
  13. theorem OAI.MetricKMedian.LPBinary.Truncated.next_ofFn line 63