OAI/Combinatorics/IndependentSets/Expansion/Capped.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LargeIndependentSets.ShortestPaths.Capped line 8
2. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.ext line 15
3. def OAI.LargeIndependentSets.ShortestPaths.Capped.finEquiv line 18
4. instance OAI.LargeIndependentSets.ShortestPaths.Capped.(instance at line 24) line 24
5. instance OAI.LargeIndependentSets.ShortestPaths.Capped.(instance at line 26) line 26
6. instance OAI.LargeIndependentSets.ShortestPaths.Capped.(instance at line 27) line 27
7. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.min_val line 29
8. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.add_val line 33
9. def OAI.LargeIndependentSets.ShortestPaths.Capped.clip line 35
10. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.clip_top line 38
11. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.clip_nat line 39
12. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.clip_min line 41
13. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.clip_add line 55
14. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.clip_le_iff line 68
15. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.closure_exact line 74
16. abbrev OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix line 83
17. def OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.get line 85
18. def OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.pivot line 87
19. def OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.run line 90
20. lemma OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.run_get line 94
21. def OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.allPairs line 105
22. def OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.ofInteger line 107
23. theorem OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.allPairs_exact line 110
24. theorem OAI.LargeIndependentSets.ShortestPaths.Capped.Matrix.threshold_exact line 118