OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalTensor.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntervalBar.Diagram.tensorObj line 19
  2. def OAI.IntervalBar.Diagram.tensorHom line 22
  3. lemma OAI.IntervalBar.Diagram.tensorObj_obj line 25
  4. lemma OAI.IntervalBar.Diagram.tensorObj_unit line 27
  5. lemma OAI.IntervalBar.Diagram.tensorObj_cut line 29
  6. lemma OAI.IntervalBar.Diagram.tensorHom_app line 33
  7. lemma OAI.IntervalBar.Diagram.associator_unit_square line 37
  8. lemma OAI.IntervalBar.Diagram.associator_cut_square line 46
  9. lemma OAI.IntervalBar.Diagram.leftUnitor_cut_square line 57
  10. lemma OAI.IntervalBar.Diagram.rightUnitor_cut_square line 63
  11. def OAI.IntervalBar.Diagram.associatorHom line 69
  12. def OAI.IntervalBar.Diagram.leftUnitorHom line 76
  13. def OAI.IntervalBar.Diagram.rightUnitorHom line 83
  14. instance OAI.IntervalBar.Diagram.monoidalStruct line 90
  15. lemma OAI.IntervalBar.Diagram.whiskerLeft_app line 100
  16. lemma OAI.IntervalBar.Diagram.whiskerRight_app line 104
  17. lemma OAI.IntervalBar.Diagram.associator_app line 108
  18. lemma OAI.IntervalBar.Diagram.leftUnitor_app line 110
  19. lemma OAI.IntervalBar.Diagram.rightUnitor_app line 112
  20. lemma OAI.IntervalBar.Diagram.tensor_app line 114
  21. lemma OAI.IntervalBar.Diagram.tensor_obj line 116
  22. lemma OAI.IntervalBar.Diagram.tensorUnit_obj line 118
  23. instance OAI.IntervalBar.Diagram.monoidal line 121
  24. instance OAI.IntervalBar.Diagram.evalMonoidal line 133
  25. lemma OAI.IntervalBar.Diagram.braiding_unit_square line 143
  26. lemma OAI.IntervalBar.Diagram.braiding_cut_square line 150
  27. def OAI.IntervalBar.Diagram.braidingHom line 158
  28. lemma OAI.IntervalBar.Diagram.inv_app line 164
  29. lemma OAI.IntervalBar.Diagram.associator_inv_app line 169
  30. instance OAI.IntervalBar.Diagram.braided line 176
  31. lemma OAI.IntervalBar.Diagram.braiding_app line 199
  32. instance OAI.IntervalBar.Diagram.symmetric line 202
  33. instance OAI.IntervalBar.Diagram.evalEquivalence line 205
  34. def OAI.IntervalBar.Diagram.evaluationEquivalence line 207