OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalBar.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IntervalBar.Diagram line 15
2. structure OAI.IntervalBar.Diagram.Hom line 30
3. lemma OAI.IntervalBar.Diagram.Hom.ext line 37
4. def OAI.IntervalBar.Diagram.Hom.id line 44
5. def OAI.IntervalBar.Diagram.Hom.comp line 49
6. def OAI.IntervalBar.Diagram.Hom.inv line 55
7. instance OAI.IntervalBar.Diagram.(instance at line 64) line 64
8. lemma OAI.IntervalBar.Diagram.id_app line 75
9. lemma OAI.IntervalBar.Diagram.comp_app line 77
10. def OAI.IntervalBar.Diagram.reindexObj line 81
11. def OAI.IntervalBar.Diagram.reindex line 90
12. lemma OAI.IntervalBar.Diagram.reindex_id line 97
13. lemma OAI.IntervalBar.Diagram.reindex_comp line 103
14. def OAI.IntervalBar.Diagram.eval line 109
15. lemma OAI.IntervalBar.Diagram.hom_ext_elementary line 113
16. instance OAI.IntervalBar.Diagram.(instance at line 136) line 136
17. def OAI.IntervalBar.Diagram.simplicial line 140