OAI/RepresentationTheory/UniversalSquare/Band/OutputBands.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Output Bands.

  1. structure OAI.Saxl.Balance.OutputBands line 14
  2. def OAI.Saxl.Balance.OutputBands.Allows line 20
  3. def OAI.Saxl.Balance.OutputBands.label line 23
  4. lemma OAI.Saxl.Balance.OutputBands.label_spec line 27
  5. lemma OAI.Saxl.Balance.OutputBands.unique line 32
  6. lemma OAI.Saxl.Balance.OutputBands.label_iff line 42
  7. lemma OAI.Saxl.Balance.OutputBands.ordered line 54
  8. def OAI.Saxl.Balance.OutputBands.alphabet line 60
  9. def OAI.Saxl.Balance.OutputBands.letterLabel line 63
  10. lemma OAI.Saxl.Balance.OutputBands.letter_iff line 66
  11. lemma OAI.Saxl.Balance.OutputBands.letter_ordered line 71