OAI/RepresentationTheory/UniversalSquare/Band/BandSeparated.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Band Separated.

  1. def OAI.UniversalTensorSquare.candidateBandPattern line 16
  2. def OAI.UniversalTensorSquare.candidatePathWord line 22
  3. def OAI.UniversalTensorSquare.candidateExtrasWord line 26
  4. theorem OAI.UniversalTensorSquare.candidateBandPattern_factor line 36
  5. lemma OAI.UniversalTensorSquare.candidateNECell_swap_not_mem line 55
  6. lemma OAI.UniversalTensorSquare.candidateBandWord_sector_iff line 63
  7. theorem OAI.UniversalTensorSquare.candidateBandWord_separated line 119