OAI/RepresentationTheory/UniversalSquare/Finite/SmallContracts13_5.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Small Contracts 13 5.

  1. def OAI.UniversalTensorSquare.smallB13_20 line 15
  2. def OAI.UniversalTensorSquare.smallT13_20 line 16
  3. def OAI.UniversalTensorSquare.smallFlag13_20 line 17
  4. lemma OAI.UniversalTensorSquare.smallCert13_20 line 18
  5. lemma OAI.UniversalTensorSquare.smallSupport13_20 line 22
  6. def OAI.UniversalTensorSquare.smallB13_21 line 31
  7. def OAI.UniversalTensorSquare.smallT13_21 line 32
  8. def OAI.UniversalTensorSquare.smallFlag13_21 line 33
  9. lemma OAI.UniversalTensorSquare.smallCert13_21 line 34
  10. lemma OAI.UniversalTensorSquare.smallSupport13_21 line 38
  11. def OAI.UniversalTensorSquare.smallB13_22 line 47
  12. def OAI.UniversalTensorSquare.smallT13_22 line 48
  13. def OAI.UniversalTensorSquare.smallFlag13_22 line 49
  14. lemma OAI.UniversalTensorSquare.smallCert13_22 line 50
  15. lemma OAI.UniversalTensorSquare.smallSupport13_22 line 54
  16. def OAI.UniversalTensorSquare.smallB13_23 line 63
  17. def OAI.UniversalTensorSquare.smallT13_23 line 64
  18. def OAI.UniversalTensorSquare.smallFlag13_23 line 65
  19. lemma OAI.UniversalTensorSquare.smallCert13_23 line 66
  20. lemma OAI.UniversalTensorSquare.smallSupport13_23 line 70