OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalMap.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IntervalBar.Diagram.mapObj line 18
  2. def OAI.IntervalBar.Diagram.map line 41
  3. def OAI.IntervalBar.Diagram.pair line 54
  4. def OAI.IntervalBar.Diagram.pairHom line 63
  5. def OAI.IntervalBar.Diagram.constantUnit line 69
  6. lemma OAI.IntervalBar.tensorμ_braiding line 87
  7. def OAI.IntervalBar.Normal.fold line 106
  8. def OAI.IntervalBar.Normal.appendIso line 110
  9. lemma OAI.IntervalBar.Normal.segment_append line 114
  10. def OAI.IntervalBar.Normal.segment line 120
  11. lemma OAI.IntervalBar.Normal.segment_self line 121
  12. def OAI.IntervalBar.Normal.diagram line 124
  13. lemma OAI.IntervalBar.Normal.project_whiskerLeft line 134
  14. lemma OAI.IntervalBar.Normal.project_whiskerRight line 138
  15. lemma OAI.IntervalBar.Normal.project_leftUnitor line 143
  16. lemma OAI.IntervalBar.Normal.project_rightUnitor line 145
  17. lemma OAI.IntervalBar.Normal.project_associator line 147
  18. def OAI.IntervalBar.Normal.projectDiagram line 152
  19. lemma OAI.IntervalBar.Normal.segment_finRange line 169
  20. def OAI.IntervalBar.Normal.elementaryDiagram line 177
  21. def OAI.IntervalBar.Normal.elementaryIso line 180
  22. instance OAI.IntervalBar.Normal.(instance at line 193) line 193