OAI/Combinatorics/MatchingCount/Sampling/MarkBridge.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MatchingFPRAS.RationalSource.sourceEdgeEquiv_centralline 26 - lemma
OAI.MatchingFPRAS.RationalSource.probePortion_castline 29 - lemma
OAI.MatchingFPRAS.RationalSource.portions_castline 42 - def
OAI.MatchingFPRAS.RationalSource.sourceMarkedEquivline 51 - lemma
OAI.MatchingFPRAS.RationalSource.portions_collapseline 55 - lemma
OAI.MatchingFPRAS.RationalSource.markedLaw_eqline 60 - lemma
OAI.MatchingFPRAS.RationalSource.markedLaw_equivline 76