OAI/RepresentationTheory/UniversalSquare/Support/Neighboring.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Neighboring.

  1. def OAI.Saxl.Balance.output line 18
  2. def OAI.Saxl.Balance.inOutputs line 22
  3. lemma OAI.Saxl.Balance.inOutputs_invariant line 25
  4. def OAI.Saxl.Balance.reverseShortColumn line 34
  5. lemma OAI.Saxl.Balance.reverseShortColumn_invol line 36
  6. def OAI.Saxl.Balance.reverseShortColumns line 41
  7. def OAI.Saxl.Balance.neighborLayer line 70
  8. def OAI.Saxl.Balance.neighborTableau line 73
  9. def OAI.Saxl.Balance.neighborRight line 76
  10. lemma OAI.Saxl.Balance.neighborLayer_row line 79
  11. lemma OAI.Saxl.Balance.neighborLayer_col line 83
  12. lemma OAI.Saxl.Balance.neighborLayer_col_iff line 90
  13. lemma OAI.Saxl.Balance.neighborLayer_group line 99
  14. lemma OAI.Saxl.Balance.neighborLayer_polytabloid line 107
  15. lemma OAI.Saxl.Balance.neighbor_outputs line 116
  16. def OAI.Saxl.Balance.neighborLetter line 127
  17. lemma OAI.Saxl.Balance.letterLift_comp line 132
  18. lemma OAI.Saxl.Balance.neighbor_left_word line 146
  19. lemma OAI.Saxl.Balance.neighbor_move line 154
  20. lemma OAI.Saxl.Balance.neighbor_right_word line 164
  21. lemma OAI.Saxl.Balance.neighbor_pair_word line 172
  22. theorem OAI.Saxl.Balance.neighboring line 182