OAI/Combinatorics/MatchingCount/Graphs/SafeTrace.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- inductive
OAI.MatchingFPRAS.SafeTrace.Pathline 11 - lemma
OAI.MatchingFPRAS.SafeTrace.Path.singleline 19 - lemma
OAI.MatchingFPRAS.SafeTrace.Path.transline 21 - lemma
OAI.MatchingFPRAS.SafeTrace.Path.run_eqline 26 - lemma
OAI.MatchingFPRAS.SafeTrace.Path.monotoneline 31 - lemma
OAI.MatchingFPRAS.SafeTrace.Path.of_runline 36 - theorem
OAI.MatchingFPRAS.SafeTrace.Path.physicalline 46 - lemma
OAI.MatchingFPRAS.SafeTrace.Path.with_supportline 76