OAI/Combinatorics/MatchingCount/Tapes/FixedEncoding.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MatchingFPRAS.FixedEncoding.encline 8 - lemma
OAI.MatchingFPRAS.FixedEncoding.blankline 11 - lemma
OAI.MatchingFPRAS.FixedEncoding.injectiveline 16 - def
OAI.MatchingFPRAS.FixedEncoding.decline 29 - lemma
OAI.MatchingFPRAS.FixedEncoding.left_inverseline 30 - lemma
OAI.MatchingFPRAS.FixedEncoding.bitsWord_lengthline 32