OAI/GroupTheory/SimpleAmenable/Simplicial/InducedMonoidal.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InducedMonoidal.Cat line 14
2. abbrev OAI.InducedMonoidal.inclusion line 15
3. instance OAI.InducedMonoidal.monoidalStruct line 16
4. def OAI.InducedMonoidal.data line 25
5. instance OAI.InducedMonoidal.monoidal line 46
6. instance OAI.InducedMonoidal.inclusionMonoidal line 47
7. def OAI.InducedMonoidal.source line 48
8. instance OAI.InducedMonoidal.sourceMonoidal line 53
9. instance OAI.InducedMonoidal.braided line 84
10. instance OAI.InducedMonoidal.inclusionBraided line 90
11. instance OAI.InducedMonoidal.sourceBraided line 94
12. instance OAI.InducedMonoidal.symmetric line 101
13. instance OAI.RestrictedNerve.posDiagramIsIso line 115
14. instance OAI.RestrictedNerve.posDiagramGroupoid line 119
15. instance OAI.RestrictedNerve.posDiagramMonoidal line 121
16. instance OAI.RestrictedNerve.posDiagramBraided line 123
17. instance OAI.RestrictedNerve.posDiagramSymmetric line 125
18. instance OAI.RestrictedNerve.diagramPropertyInverse line 127
19. lemma OAI.RestrictedNerve.diagram_μ_app line 136
20. lemma OAI.RestrictedNerve.diagram_δ_app line 138
21. lemma OAI.RestrictedNerve.posTensor_app line 144
22. lemma OAI.RestrictedNerve.posWhiskerLeft_app line 149
23. lemma OAI.RestrictedNerve.posWhiskerRight_app line 154
24. lemma OAI.RestrictedNerve.posAssoc_app line 159
25. lemma OAI.RestrictedNerve.posLeft_app line 163
26. lemma OAI.RestrictedNerve.posRight_app line 165
27. lemma OAI.RestrictedNerve.posBraiding_app line 167
28. instance OAI.RestrictedNerve.diagramPropertyMonoidal line 170
29. instance OAI.RestrictedNerve.diagramPropertyBraided line 203