OAI/Combinatorics/KMedian/Programs/NearestListProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.LPBinary.sum_map_filter_ofFn line 13
  2. abbrev OAI.MetricKMedian.LPBinary.Nearest.Entry line 24
  3. abbrev OAI.MetricKMedian.LPBinary.Nearest.ee line 25
  4. abbrev OAI.MetricKMedian.LPBinary.Nearest.ees line 26
  5. def OAI.MetricKMedian.LPBinary.Nearest.entries line 28
  6. def OAI.MetricKMedian.LPBinary.Nearest.before line 32
  7. def OAI.MetricKMedian.LPBinary.Nearest.prior line 33
  8. def OAI.MetricKMedian.LPBinary.Nearest.amount line 34
  9. def OAI.MetricKMedian.LPBinary.Nearest.filling line 35
  10. theorem OAI.MetricKMedian.LPBinary.Nearest.entries_ofFn line 37
  11. theorem OAI.MetricKMedian.LPBinary.Nearest.prior_ofFn line 41
  12. theorem OAI.MetricKMedian.LPBinary.Nearest.filling_ofFn line 46
  13. def OAI.MetricKMedian.LPBinary.Nearest.entriesProgram line 53
  14. def OAI.MetricKMedian.LPBinary.Nearest.beforeProgram line 58
  15. def OAI.MetricKMedian.LPBinary.Nearest.priorProgram line 66
  16. def OAI.MetricKMedian.LPBinary.Nearest.amountProgram line 71
  17. def OAI.MetricKMedian.LPBinary.Nearest.fillingProgram line 75