OAI/Combinatorics/KMedian/Programs/SplitListProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Preparation.RationalSplitting.Program.Raw line 16
  2. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.view line 17
  3. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.cutsData line 19
  4. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.cutsData_poly line 21
  5. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.cutsData_view line 29
  6. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.piecesData line 38
  7. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.piecesData_poly line 40
  8. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.piecesData_view line 45
  9. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.originalData line 56
  10. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.originalData_poly line 57
  11. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.originalData_view line 58
  12. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.previousData line 62
  13. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.previousData_poly line 63
  14. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.previousData_view line 69
  15. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.weightsData line 75
  16. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.weightsData_poly line 76
  17. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.weightsData_view line 77
  18. def OAI.MetricKMedian.Preparation.RationalSplitting.Program.assignedData line 83
  19. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.assignedData_poly line 84
  20. theorem OAI.MetricKMedian.Preparation.RationalSplitting.Program.assignedData_view line 89