OAI/Combinatorics/MatchingCount/Graphs/TreeRankPlan.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.ExecutableHierarchy.rankLe line 13
2. instance OAI.MatchingFPRAS.ExecutableHierarchy.(instance at line 14) line 14
3. instance OAI.MatchingFPRAS.ExecutableHierarchy.(instance at line 15) line 15
4. instance OAI.MatchingFPRAS.ExecutableHierarchy.(instance at line 16) line 16
5. instance OAI.MatchingFPRAS.ExecutableHierarchy.(instance at line 17) line 17
6. def OAI.MatchingFPRAS.ExecutableHierarchy.rankLeRealizer line 19
7. lemma OAI.MatchingFPRAS.ExecutableHierarchy.polynomial_rankLe line 27
8. def OAI.MatchingFPRAS.ExecutableHierarchy.rankEntries line 32
9. def OAI.MatchingFPRAS.ExecutableHierarchy.rankEntriesRealizer line 33
10. lemma OAI.MatchingFPRAS.ExecutableHierarchy.polynomial_rankEntries line 35
11. def OAI.MatchingFPRAS.ExecutableHierarchy.rankPlan line 42
12. def OAI.MatchingFPRAS.ExecutableHierarchy.rankPlanRealizer line 43
13. lemma OAI.MatchingFPRAS.ExecutableHierarchy.polynomial_rankPlan line 44
14. lemma OAI.MatchingFPRAS.ExecutableHierarchy.rankEntries_ofFn line 47
15. lemma OAI.MatchingFPRAS.ExecutableHierarchy.zipIdx_rankLE line 54
16. lemma OAI.MatchingFPRAS.ExecutableHierarchy.zipIdx_ofFn_id line 63
17. lemma OAI.MatchingFPRAS.ExecutableHierarchy.rankPlan_eq line 69