OAI/Combinatorics/KMedian/Process/CountListOperations.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseCounts.ListOperation.Row line 12
  2. abbrev OAI.MetricKMedian.SparseCounts.ListOperation.Table line 13
  3. abbrev OAI.MetricKMedian.SparseCounts.ListOperation.er line 14
  4. abbrev OAI.MetricKMedian.SparseCounts.ListOperation.et line 15
  5. def OAI.MetricKMedian.SparseCounts.ListOperation.indices line 17
  6. theorem OAI.MetricKMedian.SparseCounts.ListOperation.indices_poly line 18
  7. def OAI.MetricKMedian.SparseCounts.ListOperation.view line 20
  8. def OAI.MetricKMedian.SparseCounts.ListOperation.setView line 21
  9. def OAI.MetricKMedian.SparseCounts.ListOperation.edges line 22
  10. def OAI.MetricKMedian.SparseCounts.ListOperation.featureList line 24
  11. def OAI.MetricKMedian.SparseCounts.ListOperation.nextTable line 25
  12. def OAI.MetricKMedian.SparseCounts.ListOperation.dimensions line 27
  13. theorem OAI.MetricKMedian.SparseCounts.ListOperation.edges_poly line 31
  14. theorem OAI.MetricKMedian.SparseCounts.ListOperation.featureList_poly line 36
  15. theorem OAI.MetricKMedian.SparseCounts.ListOperation.nextTable_poly line 37
  16. theorem OAI.MetricKMedian.SparseCounts.ListOperation.dimensions_poly line 40
  17. theorem OAI.MetricKMedian.SparseCounts.ListOperation.edges_view line 47
  18. theorem OAI.MetricKMedian.SparseCounts.ListOperation.featureList_view line 56
  19. theorem OAI.MetricKMedian.SparseCounts.ListOperation.nextTable_view line 72
  20. theorem OAI.MetricKMedian.SparseCounts.ListOperation.dimensions_eq line 86