OAI/Combinatorics/KMedian/Programs/FinalSelectionProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.Program.feasible line 15
  2. def OAI.MetricKMedian.Reduction.Program.feasibleData line 16
  3. theorem OAI.MetricKMedian.Reduction.Program.feasibleData_poly line 17
  4. theorem OAI.MetricKMedian.Reduction.Program.feasibleData_view line 18
  5. def OAI.MetricKMedian.Reduction.Program.annotateData line 20
  6. theorem OAI.MetricKMedian.Reduction.Program.annotateData_poly line 22
  7. def OAI.MetricKMedian.Reduction.Program.selectRaw line 23
  8. theorem OAI.MetricKMedian.Reduction.Program.selectRaw_poly line 24
  9. theorem OAI.MetricKMedian.Reduction.Program.selectRaw_view line 25
  10. def OAI.MetricKMedian.Reduction.Program.selectList line 34
  11. def OAI.MetricKMedian.Reduction.Program.selectData line 36
  12. theorem OAI.MetricKMedian.Reduction.Program.selectData_poly line 37
  13. theorem OAI.MetricKMedian.Reduction.Program.selectData_view line 38
  14. theorem OAI.MetricKMedian.Reduction.Program.selectList_spec line 44