OAI/RepresentationTheory/UniversalSquare/Capacity/Intermediate.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Intermediate.

  1. def OAI.UniversalTensorSquare.testWidth line 15
  2. lemma OAI.UniversalTensorSquare.testWidth_valid line 17
  3. def OAI.UniversalTensorSquare.prefixBounds line 27
  4. lemma OAI.UniversalTensorSquare.prefixBounds_sound line 34
  5. def OAI.UniversalTensorSquare.exceptionalPair line 61
  6. instance OAI.UniversalTensorSquare.(instance at line 65) line 65
  7. def OAI.UniversalTensorSquare.admissibleR line 69
  8. instance OAI.UniversalTensorSquare.(instance at line 72) line 72
  9. def OAI.UniversalTensorSquare.intermediateCheck line 76
  10. instance OAI.UniversalTensorSquare.(instance at line 80) line 80
  11. lemma OAI.UniversalTensorSquare.intermediate9 line 85
  12. lemma OAI.UniversalTensorSquare.intermediate10 line 88
  13. lemma OAI.UniversalTensorSquare.intermediate11 line 91
  14. lemma OAI.UniversalTensorSquare.intermediate12 line 94
  15. lemma OAI.UniversalTensorSquare.intermediate13 line 97
  16. lemma OAI.UniversalTensorSquare.intermediate14 line 100
  17. lemma OAI.UniversalTensorSquare.intermediate15 line 103
  18. lemma OAI.UniversalTensorSquare.intermediate16 line 106
  19. lemma OAI.UniversalTensorSquare.intermediate17 line 109
  20. lemma OAI.UniversalTensorSquare.intermediate18 line 112
  21. lemma OAI.UniversalTensorSquare.intermediate19 line 115
  22. lemma OAI.UniversalTensorSquare.intermediate20 line 118
  23. lemma OAI.UniversalTensorSquare.intermediate21 line 121
  24. lemma OAI.UniversalTensorSquare.capacity_intermediate_numeric line 124
  25. lemma OAI.UniversalTensorSquare.first_prefix_height line 151
  26. theorem OAI.UniversalTensorSquare.capacity_intermediate line 167