OAI/RepresentationTheory/UniversalSquare/Band/BandGluing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Band Gluing.

  1. def OAI.Saxl.FlagColumns.columnsAway line 15
  2. lemma OAI.Saxl.FlagColumns.clearSlots_of_columnsAway line 19
  3. def OAI.Saxl.joinedPositionEquiv line 47
  4. lemma OAI.Saxl.joinedPositionEquiv_left line 52
  5. lemma OAI.Saxl.joinedPositionEquiv_right line 58
  6. lemma OAI.Saxl.relabelWord_positionProduct line 64
  7. lemma OAI.Saxl.joinedPositionEquiv_isLeft line 80
  8. lemma OAI.Saxl.wordSector_joinedPositionEquiv line 87
  9. lemma OAI.Saxl.coordinateProjection_relabel_split line 98
  10. theorem OAI.UniversalTensorSquare.candidateBandWord_support_of_columns line 116