OAI/Combinatorics/KMedian/Optimization/LPListFacts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.LPBinary.Row line 12
  2. abbrev OAI.MetricKMedian.LPBinary.Rows line 13
  3. abbrev OAI.MetricKMedian.LPBinary.er line 14
  4. abbrev OAI.MetricKMedian.LPBinary.ers line 15
  5. theorem OAI.MetricKMedian.LPBinary.foldl_max_le line 17
  6. theorem OAI.MetricKMedian.LPBinary.le_foldl_max line 24
  7. theorem OAI.MetricKMedian.LPBinary.member_le_foldl_max line 29
  8. theorem OAI.MetricKMedian.LPBinary.foldl_max_eq line 37
  9. theorem OAI.MetricKMedian.LPBinary.sum_filter_ofFn line 41
  10. theorem OAI.MetricKMedian.LPBinary.length_filter_ofFn line 52
  11. def OAI.MetricKMedian.LPBinary.Program.ratMax line 64
  12. def OAI.MetricKMedian.LPBinary.Program.ratMin line 69
  13. def OAI.MetricKMedian.LPBinary.Program.maxFold line 74