OAI/Combinatorics/MatchingCount/Machines/TreeGuideTables.lean
16 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MatchingFPRAS.NumericLadder.slotUniverseline 10 - def
OAI.MatchingFPRAS.NumericLadder.slotUniverseRealizerline 11 - lemma
OAI.MatchingFPRAS.NumericLadder.polynomial_slotUniverseline 12 - def
OAI.MatchingFPRAS.NumericLadder.guideTestline 15 - def
OAI.MatchingFPRAS.NumericLadder.guideTestRealizerline 18 - lemma
OAI.MatchingFPRAS.NumericLadder.polynomial_guideTestline 24 - def
OAI.MatchingFPRAS.NumericLadder.guideSetline 32 - def
OAI.MatchingFPRAS.NumericLadder.guideSetRealizerline 33 - lemma
OAI.MatchingFPRAS.NumericLadder.polynomial_guideSetline 35 - def
OAI.MatchingFPRAS.NumericLadder.guideRowsline 40 - def
OAI.MatchingFPRAS.NumericLadder.guideRowsRealizerline 41 - lemma
OAI.MatchingFPRAS.NumericLadder.polynomial_guideRowsline 43 - lemma
OAI.MatchingFPRAS.NumericLadder.slotUniverse_sourceline 48 - lemma
OAI.MatchingFPRAS.NumericLadder.mem_guides_rankline 62 - lemma
OAI.MatchingFPRAS.NumericLadder.guideSet_sourceline 78 - lemma
OAI.MatchingFPRAS.NumericLadder.guideRows_sourceline 92