OAI/RepresentationTheory/UniversalSquare/Band/BandPath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Band Path.

  1. def OAI.UniversalTensorSquare.candidatePathEquiv line 17
  2. def OAI.UniversalTensorSquare.bandSmallRowLetter line 20
  3. def OAI.UniversalTensorSquare.bandSmallColLetter line 24
  4. lemma OAI.UniversalTensorSquare.candidatePathRow_eq line 28
  5. lemma OAI.UniversalTensorSquare.candidatePathCol_eq line 54
  6. def OAI.UniversalTensorSquare.bandPairSmallLetter line 88
  7. lemma OAI.UniversalTensorSquare.bandPairSmallLetter_injective line 92
  8. theorem OAI.UniversalTensorSquare.candidatePathWord_eq line 96
  9. theorem OAI.UniversalTensorSquare.candidatePathWord_support line 111