OAI/RepresentationTheory/UniversalSquare/Band/TwoPathGeometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Two Path Geometry.

  1. def OAI.Saxl.Balance.appendShortMap line 17
  2. lemma OAI.Saxl.Balance.appendShortMap_injective line 30
  3. def OAI.Saxl.Balance.appendShortCells line 74
  4. lemma OAI.Saxl.Balance.appendShortCells_left line 86
  5. lemma OAI.Saxl.Balance.appendShortCells_right line 91
  6. lemma OAI.Saxl.Balance.appendShortCells_column_same line 96
  7. lemma OAI.Saxl.Balance.appendShortCells_left_col line 118
  8. lemma OAI.Saxl.Balance.appendShortCells_right_col line 127
  9. def OAI.Saxl.Balance.appendShortTableau line 136
  10. lemma OAI.Saxl.Balance.appendShort_polytabloid line 142
  11. def OAI.Saxl.Balance.twoPathLeft line 198
  12. def OAI.Saxl.Balance.twoPathRight line 203
  13. lemma OAI.Saxl.Balance.appendShortCells_left_neighbor line 209
  14. lemma OAI.Saxl.Balance.appendShortCells_right_neighbor line 217
  15. lemma OAI.Saxl.Balance.twoPathLeft_col_left line 225
  16. lemma OAI.Saxl.Balance.twoPathLeft_col_right line 233
  17. lemma OAI.Saxl.Balance.twoPathRight_col_left line 241
  18. lemma OAI.Saxl.Balance.twoPathRight_col_right line 250
  19. theorem OAI.Saxl.Balance.twoPath_outputs line 259
  20. lemma OAI.Saxl.Balance.positionProduct_swap line 281
  21. lemma OAI.Saxl.Balance.neighborLayer_reverse_word line 287
  22. lemma OAI.Saxl.Balance.twoPathLeft_word line 301
  23. lemma OAI.Saxl.Balance.twoPathRight_word line 309
  24. def OAI.Saxl.Balance.twoPathLetter line 318
  25. lemma OAI.Saxl.Balance.twoPath_doubleTranspose_word line 324
  26. lemma OAI.Saxl.Balance.twoPath_pair_word line 332
  27. theorem OAI.Saxl.Balance.two_paths line 361