OAI/Combinatorics/MatchingCount/Machines/TreeBuild.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.ExecutableSource.vertices_eq_ofFn_length line 13
2. abbrev OAI.MatchingFPRAS.ExecutableSource.BuildInput line 19
3. def OAI.MatchingFPRAS.ExecutableSource.prepare line 21
4. def OAI.MatchingFPRAS.ExecutableSource.prepareRealizer line 22
5. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_prepare line 24
6. def OAI.MatchingFPRAS.ExecutableSource.buildMatrix line 31
7. def OAI.MatchingFPRAS.ExecutableSource.buildMatrixRealizer line 32
8. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_buildMatrix line 33
9. def OAI.MatchingFPRAS.ExecutableSource.buildClosure line 36
10. def OAI.MatchingFPRAS.ExecutableSource.buildClosureRealizer line 37
11. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_buildClosure line 38
12. lemma OAI.MatchingFPRAS.ExecutableSource.source_activity_nonneg line 41
13. lemma OAI.MatchingFPRAS.ExecutableSource.buildMatrix_repr line 51
14. lemma OAI.MatchingFPRAS.ExecutableSource.buildClosure_repr line 69