OAI/RepresentationTheory/UniversalSquare/Band/BandSplit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Band Split.

  1. lemma OAI.UniversalTensorSquare.candidateBandParts_cell line 16
  2. def OAI.UniversalTensorSquare.candidateBandSplit line 28
  3. def OAI.UniversalTensorSquare.candidateExtraSplit line 34
  4. lemma OAI.UniversalTensorSquare.candidateBandSplit_path line 37
  5. lemma OAI.UniversalTensorSquare.candidateBandSplit_NE line 44
  6. lemma OAI.UniversalTensorSquare.candidateBandSplit_SW line 55
  7. lemma OAI.UniversalTensorSquare.candidatePathCell_row_tag line 66
  8. lemma OAI.UniversalTensorSquare.candidatePathCell_swap line 75
  9. lemma OAI.UniversalTensorSquare.candidateSeparatedRow_path line 83
  10. lemma OAI.UniversalTensorSquare.candidateParts_row_sectors line 93
  11. lemma OAI.UniversalTensorSquare.candidateBandRow_sector_eq line 123