OAI/Combinatorics/IndependentSets/Reduction/CircleCost.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.ShortestPaths.circleCost line 10
  2. lemma OAI.LargeIndependentSets.ShortestPaths.circleCost_dist line 13
  3. lemma OAI.LargeIndependentSets.ShortestPaths.circleCost_edist line 19
  4. lemma OAI.LargeIndependentSets.ShortestPaths.natSupCast line 25
  5. def OAI.LargeIndependentSets.ShortestPaths.copyCost line 39
  6. lemma OAI.LargeIndependentSets.ShortestPaths.copyCost_exact line 45
  7. lemma OAI.LargeIndependentSets.ShortestPaths.forwardZero_iff line 54
  8. instance OAI.LargeIndependentSets.ShortestPaths.forwardZero_decidable line 68
  9. instance OAI.LargeIndependentSets.ShortestPaths.zeroLink_decidable line 74
  10. def OAI.LargeIndependentSets.ShortestPaths.linkCost line 80
  11. lemma OAI.LargeIndependentSets.ShortestPaths.linkCost_exact line 86
  12. lemma OAI.LargeIndependentSets.ShortestPaths.scaled_min line 96
  13. lemma OAI.LargeIndependentSets.ShortestPaths.Matrix.scaled_allPairs_exact line 104
  14. lemma OAI.LargeIndependentSets.ShortestPaths.walkLength_reindex line 114
  15. lemma OAI.LargeIndependentSets.ShortestPaths.pathDistance_reindex line 121
  16. def OAI.LargeIndependentSets.ShortestPaths.gridMatrix line 135
  17. theorem OAI.LargeIndependentSets.ShortestPaths.grid_allPairs_exact line 141