OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedMonoidal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.RestrictedNerve.restricted_isIso line 16
  2. instance OAI.RestrictedNerve.restricted_groupoid line 21
  3. instance OAI.RestrictedNerve.strings_inverse line 23
  4. instance OAI.RestrictedNerve.strings_isIso line 27
  5. instance OAI.RestrictedNerve.strings_groupoid line 35
  6. lemma OAI.RestrictedNerve.wide_hom_inv line 38
  7. lemma OAI.RestrictedNerve.wide_inv_hom line 41
  8. instance OAI.RestrictedNerve.strings_monoidal line 48
  9. instance OAI.RestrictedNerve.strings_braided line 61
  10. abbrev OAI.RestrictedNerve.inclusion line 64
  11. instance OAI.RestrictedNerve.inclusionMonoidal line 65
  12. instance OAI.RestrictedNerve.inclusionBraided line 74
  13. instance OAI.RestrictedNerve.reindexMonoidal line 78
  14. instance OAI.RestrictedNerve.reindexBraided line 121
  15. abbrev OAI.RestrictedNerve.diagramInclusion line 135
  16. abbrev OAI.RestrictedNerve.PosDiagrams line 136
  17. def OAI.RestrictedNerve.diagramProperty line 137
  18. instance OAI.RestrictedNerve.diagramProperty_multiplicative line 139
  19. def OAI.RestrictedNerve.stringVertex line 146
  20. def OAI.RestrictedNerve.stringVertexMap line 176
  21. def OAI.RestrictedNerve.transposeDiagramObj line 191
  22. def OAI.RestrictedNerve.transposeDiagramHom line 201
  23. def OAI.RestrictedNerve.transposeDiagram line 219
  24. def OAI.RestrictedNerve.untransposeDiagramObj line 228
  25. def OAI.RestrictedNerve.untransposeDiagramHom line 307
  26. def OAI.RestrictedNerve.untransposeDiagram line 333
  27. def OAI.RestrictedNerve.diagramEquivalence line 342
  28. instance OAI.RestrictedNerve.(instance at line 351) line 351