OAI/RepresentationTheory/UniversalSquare/Band/BandLetters.lean
14 declarations, 0 contain sorry, 0 declared as axioms
Band Letters.
- lemma
OAI.UniversalTensorSquare.candidateSeparatedRow_NEline 16 - lemma
OAI.UniversalTensorSquare.candidateSeparatedRow_SWline 27 - lemma
OAI.UniversalTensorSquare.shortColumns_widthline 37 - def
OAI.UniversalTensorSquare.bandSmallLetterline 46 - lemma
OAI.UniversalTensorSquare.bandSmallLetter_injectiveline 48 - def
OAI.UniversalTensorSquare.bandExtraLetterline 51 - lemma
OAI.UniversalTensorSquare.bandExtraLetter_injectiveline 58 - lemma
OAI.UniversalTensorSquare.bandExtraLetter_highline 66 - lemma
OAI.UniversalTensorSquare.candidateRowAlphabet_sizeline 72 - lemma
OAI.UniversalTensorSquare.candidateColAlphabet_sizeline 77 - lemma
OAI.UniversalTensorSquare.candidateBandRowSeed_NEline 82 - lemma
OAI.UniversalTensorSquare.candidateBandRowSeed_SWline 93 - lemma
OAI.UniversalTensorSquare.candidateBandColSeed_NEline 106 - lemma
OAI.UniversalTensorSquare.candidateBandColSeed_SWline 121