OAI/Combinatorics/MatchingCount/Algorithm/OnlineLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.OnlineStage.vertexCount line 17
2. abbrev OAI.MatchingFPRAS.OnlineStage.labelCount line 18
3. abbrev OAI.MatchingFPRAS.OnlineStage.edgeCount line 19
4. abbrev OAI.MatchingFPRAS.OnlineStage.tierCount line 20
5. abbrev OAI.MatchingFPRAS.OnlineStage.copies line 21
6. abbrev OAI.MatchingFPRAS.OnlineStage.scansCount line 22
7. abbrev OAI.MatchingFPRAS.OnlineStage.choiceWidth line 23
8. abbrev OAI.MatchingFPRAS.OnlineStage.markWidth line 26
9. abbrev OAI.MatchingFPRAS.OnlineStage.Raw line 27
10. def OAI.MatchingFPRAS.OnlineStage.rawEquiv line 30
11. lemma OAI.MatchingFPRAS.OnlineStage.raw_scan line 35
12. lemma OAI.MatchingFPRAS.OnlineStage.raw_marks line 39
13. def OAI.MatchingFPRAS.OnlineStage.rawDraw line 41
14. def OAI.MatchingFPRAS.OnlineStage.core line 47
15. lemma OAI.MatchingFPRAS.OnlineStage.generated_eq_core line 60
16. lemma OAI.MatchingFPRAS.OnlineStage.generated_eq_raw line 68
17. lemma OAI.MatchingFPRAS.OnlineStage.rawDraw_law line 84