OAI/Combinatorics/MatchingCount/Machines/TreeReach.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.TreeTyped.weight_subperm line 11
2. lemma OAI.MatchingFPRAS.TreeTyped.weight_finset_subset line 15
3. lemma OAI.MatchingFPRAS.TreeTyped.weight_finset_union line 20
4. abbrev OAI.MatchingFPRAS.TreeTyped.FiniteReach.Input line 31
5. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.grow line 33
6. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.sweep line 35
7. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.reach line 36
8. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.neighbor line 39
9. lemma OAI.MatchingFPRAS.TreeTyped.FiniteReach.polynomial_neighbor line 42
10. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.growRealizer line 47
11. lemma OAI.MatchingFPRAS.TreeTyped.FiniteReach.polynomial_grow line 53
12. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.sweepRealizer line 66
13. def OAI.MatchingFPRAS.TreeTyped.FiniteReach.reachRealizer line 70
14. lemma OAI.MatchingFPRAS.TreeTyped.FiniteReach.polynomial_reach line 76
15. lemma OAI.MatchingFPRAS.TreeTyped.FiniteReach.countDown_sweep line 116
16. lemma OAI.MatchingFPRAS.TreeTyped.FiniteReach.reach_eq line 125