OAI/Combinatorics/IndependentSets/Reduction/Total.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.SemanticReduction.total line 14
  2. def OAI.LargeIndependentSets.SemanticReduction.totalPolynomial line 17
  3. lemma OAI.LargeIndependentSets.SemanticReduction.total_output_bound line 20
  4. theorem OAI.LargeIndependentSets.total_semantic_polynomial_output_reduction line 30
  5. def OAI.LargeIndependentSets.ShortestPaths.pivot line 50
  6. def OAI.LargeIndependentSets.ShortestPaths.closure line 53
  7. lemma OAI.LargeIndependentSets.ShortestPaths.pivot_le line 57
  8. lemma OAI.LargeIndependentSets.ShortestPaths.pivot_at line 60
  9. lemma OAI.LargeIndependentSets.ShortestPaths.pivot_preserves line 65
  10. lemma OAI.LargeIndependentSets.ShortestPaths.closure_le line 84
  11. lemma OAI.LargeIndependentSets.ShortestPaths.closure_preserves line 90
  12. lemma OAI.LargeIndependentSets.ShortestPaths.closure_at line 97
  13. lemma OAI.LargeIndependentSets.ShortestPaths.distance_le_closure line 107
  14. theorem OAI.LargeIndependentSets.ShortestPaths.closure_eq_distance line 120
  15. lemma OAI.LargeIndependentSets.ShortestPaths.closure_map line 130
  16. abbrev OAI.LargeIndependentSets.ShortestPaths.Matrix line 143
  17. def OAI.LargeIndependentSets.ShortestPaths.Matrix.get line 145
  18. def OAI.LargeIndependentSets.ShortestPaths.Matrix.pivot line 147
  19. def OAI.LargeIndependentSets.ShortestPaths.Matrix.run line 151
  20. lemma OAI.LargeIndependentSets.ShortestPaths.Matrix.run_get line 155
  21. def OAI.LargeIndependentSets.ShortestPaths.Matrix.allPairs line 166
  22. theorem OAI.LargeIndependentSets.ShortestPaths.Matrix.allPairs_exact line 168