OAI/Combinatorics/KMedian/Sparse/SparseListTrim.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.LawData line 14
  2. abbrev OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.el line 15
  3. abbrev OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.er line 16
  4. abbrev OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.Data line 18
  5. abbrev OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.ed line 19
  6. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.raw line 21
  7. abbrev OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.encode line 23
  8. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.activeEntries line 25
  9. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.trimData line 27
  10. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.states_list line 30
  11. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.activeEntries_raw line 33
  12. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.trimData_raw line 39
  13. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.activeProgram line 46
  14. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.trimDataProgram line 55
  15. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.trimProgram line 63