OAI/Combinatorics/SparsestCut/Semimetrics.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.IsSemimetric line 16
  2. lemma OAI.UniformSparsestCut.NegativeType.semimetric line 20
  3. lemma OAI.UniformSparsestCut.NegativeType.scale line 27
  4. lemma OAI.UniformSparsestCut.cutDist_negativeType line 38
  5. lemma OAI.UniformSparsestCut.cut_nonempty line 53
  6. lemma OAI.UniformSparsestCut.feasible_nonempty line 62
  7. lemma OAI.UniformSparsestCut.normalized_pair_le_one line 69
  8. lemma OAI.UniformSparsestCut.continuous_pairSum line 76
  9. lemma OAI.UniformSparsestCut.semimetric_closed line 86
  10. lemma OAI.UniformSparsestCut.normalized_semimetric_compact line 101
  11. lemma OAI.UniformSparsestCut.objective_nonneg line 109
  12. lemma OAI.UniformSparsestCut.objective_pos_of_cuts line 113
  13. lemma OAI.UniformSparsestCut.glValue_pos_of_cuts line 160
  14. lemma OAI.UniformSparsestCut.OPT_ge_one_of_cuts line 176