OAI/Combinatorics/KMedian/Compression/AffineListOperations.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.Row line 14
  2. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.Rows line 15
  3. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.er line 16
  4. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.em line 17
  5. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.es line 18
  6. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.Data line 19
  7. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.ed line 20
  8. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.Entry line 21
  9. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.ee line 22
  10. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.ees line 23
  11. def OAI.MetricKMedian.IntegerLaw.ListOperation.entries line 25
  12. def OAI.MetricKMedian.IntegerLaw.ListOperation.active line 29
  13. def OAI.MetricKMedian.IntegerLaw.ListOperation.activeRows line 30
  14. def OAI.MetricKMedian.IntegerLaw.ListOperation.activeData line 32
  15. def OAI.MetricKMedian.IntegerLaw.ListOperation.extend line 35
  16. def OAI.MetricKMedian.IntegerLaw.ListOperation.full line 38
  17. structure OAI.MetricKMedian.IntegerLaw.ListOperation.Input line 42
  18. def OAI.MetricKMedian.IntegerLaw.ListOperation.Input.raw line 49
  19. abbrev OAI.MetricKMedian.IntegerLaw.ListOperation.Input.encode line 51
  20. def OAI.MetricKMedian.IntegerLaw.ListOperation.Input.kernel line 53
  21. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.indices_ofFn line 56
  22. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.range_ofFn line 61
  23. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.entries_raw line 65
  24. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.active_raw line 69
  25. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.activeRows_raw line 75
  26. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.activeData_raw line 86
  27. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.extend_ofFn line 90
  28. theorem OAI.MetricKMedian.IntegerLaw.ListOperation.full_raw line 119