OAI/RepresentationTheory/UniversalSquare/Capacity/NumericBands.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Numeric Bands.

  1. def OAI.Saxl.Balance.BandsValid line 15
  2. instance OAI.Saxl.Balance.(instance at line 19) line 19
  3. def OAI.Saxl.Balance.bandStarts line 23
  4. def OAI.Saxl.Balance.bandUpper line 25
  5. lemma OAI.Saxl.Balance.bandUpper_eq line 28
  6. lemma OAI.Saxl.Balance.mem_bandStarts line 41
  7. def OAI.Saxl.Balance.numericBands line 44
  8. lemma OAI.Saxl.Balance.numericBands_iff line 59