OAI/Combinatorics/KMedian/Rounding/TargetSubsetProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.SparseTargetSubset.Program.Input line 14
  2. abbrev OAI.MetricKMedian.SparseTargetSubset.Program.Raw line 19
  3. def OAI.MetricKMedian.SparseTargetSubset.Program.Input.raw line 20
  4. abbrev OAI.MetricKMedian.SparseTargetSubset.Program.Input.encode line 21
  5. def OAI.MetricKMedian.SparseTargetSubset.Program.Input.weighted line 23
  6. def OAI.MetricKMedian.SparseTargetSubset.Program.prepare line 25
  7. theorem OAI.MetricKMedian.SparseTargetSubset.Program.prepare_poly line 26
  8. theorem OAI.MetricKMedian.SparseTargetSubset.Program.prepare_input line 29
  9. def OAI.MetricKMedian.SparseTargetSubset.Program.Input.result line 33
  10. def OAI.MetricKMedian.SparseTargetSubset.Program.program line 34