OAI/RepresentationTheory/UniversalSquare/Capacity/RefinedExhaustion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Refined Exhaustion.

  1. def OAI.UniversalTensorSquare.RowBounds line 15
  2. def OAI.UniversalTensorSquare.minHeight line 18
  3. lemma OAI.UniversalTensorSquare.minHeight_pos line 21
  4. lemma OAI.UniversalTensorSquare.minHeight_sound line 30
  5. lemma OAI.UniversalTensorSquare.rowLen_first_le_prefix line 52
  6. def OAI.UniversalTensorSquare.impossibleBounds line 57
  7. instance OAI.UniversalTensorSquare.(instance at line 66) line 66
  8. lemma OAI.UniversalTensorSquare.impossibleBounds_false line 74
  9. lemma OAI.UniversalTensorSquare.rowPrefix_eq_take line 94
  10. lemma OAI.UniversalTensorSquare.not_dominates_witness line 109
  11. def OAI.UniversalTensorSquare.coreImpossible line 132
  12. instance OAI.UniversalTensorSquare.(instance at line 135) line 135
  13. lemma OAI.UniversalTensorSquare.coreImpossible_false line 138
  14. def OAI.UniversalTensorSquare.refinedCheck line 145
  15. instance OAI.UniversalTensorSquare.(instance at line 150) line 150
  16. theorem OAI.UniversalTensorSquare.refined_capacity_dichotomy line 153