OAI/Combinatorics/KMedian/Programs/PivotListProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.Row line 16
  2. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.er line 17
  3. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.Entry line 18
  4. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.ee line 19
  5. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.ees line 20
  6. def OAI.MetricKMedian.IntegerLaw.ListPivot.ratio line 22
  7. def OAI.MetricKMedian.IntegerLaw.ListPivot.least line 23
  8. def OAI.MetricKMedian.IntegerLaw.ListPivot.pivot line 24
  9. theorem OAI.MetricKMedian.IntegerLaw.ListPivot.least_ofFn line 26
  10. theorem OAI.MetricKMedian.IntegerLaw.ListPivot.pivot_ofFn line 38
  11. def OAI.MetricKMedian.IntegerLaw.ListPivot.ratioProgram line 55
  12. def OAI.MetricKMedian.IntegerLaw.ListPivot.positiveProgram line 57
  13. def OAI.MetricKMedian.IntegerLaw.ListPivot.leastProgram line 59
  14. def OAI.MetricKMedian.IntegerLaw.ListPivot.pivotProgram line 61
  15. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.LawData line 70
  16. abbrev OAI.MetricKMedian.IntegerLaw.ListPivot.el line 71
  17. def OAI.MetricKMedian.IntegerLaw.ListPivot.update line 73
  18. theorem OAI.MetricKMedian.IntegerLaw.ListPivot.update_ofFn line 79
  19. def OAI.MetricKMedian.IntegerLaw.ListPivot.updateProgram line 87