OAI/RepresentationTheory/UniversalSquare/Balance/BalanceBlocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Balance Blocks.

  1. def OAI.Saxl.Balance.bigColumns line 15
  2. def OAI.Saxl.Balance.bigParts line 17
  3. def OAI.Saxl.Balance.bigUpper line 19
  4. theorem OAI.Saxl.Balance.WordPacking.bigBlock line 21
  5. def OAI.Saxl.Balance.shortColumns line 40
  6. def OAI.Saxl.Balance.shortParts line 42
  7. def OAI.Saxl.Balance.shortMarks line 44
  8. theorem OAI.Saxl.Balance.WordPacking.shortBlock line 46
  9. lemma OAI.Saxl.Balance.bigParts_length line 62
  10. lemma OAI.Saxl.Balance.shortParts_length line 66
  11. lemma OAI.Saxl.Balance.oneIf_length line 71
  12. lemma OAI.Saxl.Balance.mem_shortMarks line 76
  13. lemma OAI.Saxl.Balance.mem_markIf line 87