OAI/RepresentationTheory/UniversalSquare/Band/TwoStrip.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Two Strip.

  1. def OAI.Saxl.Balance.FourInterlacing line 15
  2. lemma OAI.Saxl.Balance.four_interlacing_exists line 19
  3. lemma OAI.Saxl.Balance.horizontal_of_interlacing line 47
  4. lemma OAI.Saxl.Balance.sorted_four line 66
  5. lemma OAI.Saxl.Balance.ofRowLens_height line 71
  6. lemma OAI.Saxl.Balance.ofRowLens_rowLen line 79
  7. lemma OAI.Saxl.Balance.card_of_height_four line 86
  8. lemma OAI.Saxl.Balance.odd_column_of_row_gap line 91
  9. theorem OAI.Saxl.Balance.horizontal_two_odd_precursor line 106
  10. theorem OAI.Saxl.Balance.two_path_strip_restriction line 141