OAI/Combinatorics/SparsestCut/Metric.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformSparsestCut.SourceMetric.V line 16
  2. instance OAI.UniformSparsestCut.SourceMetric.vertexFintype line 17
  3. def OAI.UniformSparsestCut.SourceMetric.L line 20
  4. def OAI.UniformSparsestCut.SourceMetric.err line 22
  5. lemma OAI.UniformSparsestCut.SourceMetric.realization line 24
  6. def OAI.UniformSparsestCut.SourceMetric.Cā‚€ line 88
  7. lemma OAI.UniformSparsestCut.SourceMetric.Cā‚€_pos line 89
  8. def OAI.UniformSparsestCut.SourceMetric.vertex line 90
  9. lemma OAI.UniformSparsestCut.SourceMetric.near_norm line 94
  10. lemma OAI.UniformSparsestCut.SourceMetric.macro_bound line 100
  11. lemma OAI.UniformSparsestCut.SourceMetric.one_step line 136