OAI/Combinatorics/KMedian/Sparse/SparseGraphFeatures.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseGraph.Graph line 14
  2. def OAI.MetricKMedian.SparseGraph.edge line 16
  3. def OAI.MetricKMedian.SparseGraph.edgeCode line 18
  4. def OAI.MetricKMedian.SparseGraph.features line 21
  5. theorem OAI.MetricKMedian.SparseGraph.features_single line 26
  6. theorem OAI.MetricKMedian.SparseGraph.features_pair line 30
  7. def OAI.MetricKMedian.SparseGraph.next line 35
  8. theorem OAI.MetricKMedian.SparseGraph.edge_next line 38
  9. def OAI.MetricKMedian.SparseGraph.step line 42
  10. theorem OAI.MetricKMedian.SparseGraph.step_single line 46
  11. theorem OAI.MetricKMedian.SparseGraph.step_pair line 60