OAI/Combinatorics/KMedian/Reduction/DeletionProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Reduction.Program.eligibleData line 22
  2. theorem OAI.MetricKMedian.Reduction.Program.eligibleData_poly line 24
  3. theorem OAI.MetricKMedian.Reduction.Program.eligibleData_view line 25
  4. def OAI.MetricKMedian.Reduction.Program.deleteData line 33
  5. theorem OAI.MetricKMedian.Reduction.Program.deleteData_poly line 38
  6. theorem OAI.MetricKMedian.Reduction.Program.deleteData_view line 39
  7. def OAI.MetricKMedian.Reduction.Program.historyData line 52
  8. theorem OAI.MetricKMedian.Reduction.Program.historyData_poly line 55
  9. theorem OAI.MetricKMedian.Reduction.Program.historyData_view line 59
  10. def OAI.MetricKMedian.Reduction.Program.values line 65
  11. theorem OAI.MetricKMedian.Reduction.Program.values_toFinset line 68
  12. def OAI.MetricKMedian.Reduction.Program.valuesData line 77
  13. theorem OAI.MetricKMedian.Reduction.Program.valuesData_poly line 80
  14. theorem OAI.MetricKMedian.Reduction.Program.valuesData_view line 81
  15. def OAI.MetricKMedian.Reduction.Program.endpoints line 86
  16. theorem OAI.MetricKMedian.Reduction.Program.endpoints_toFinset line 88
  17. def OAI.MetricKMedian.Reduction.Program.endpointsData line 91
  18. theorem OAI.MetricKMedian.Reduction.Program.endpointsData_poly line 93
  19. theorem OAI.MetricKMedian.Reduction.Program.endpointsData_view line 99