OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalPullback.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntervalBar.Diagram.map_reindex_id line 18
2. lemma OAI.IntervalBar.Diagram.map_reindex_comp line 39
3. def OAI.IntervalBar.Diagram.reindex₂ line 64
4. lemma OAI.IntervalBar.Diagram.reindex₂_id line 68
5. lemma OAI.IntervalBar.Diagram.reindex₂_comp line 80
6. def OAI.IntervalBar.Diagram.bisimplicial line 88
7. lemma OAI.IntervalBar.Diagram.iso_hext line 106
8. lemma OAI.IntervalBar.Diagram.hom_hext line 111
9. lemma OAI.IntervalBar.Diagram.hfunext line 117
10. instance OAI.IntervalBar.Diagram.reindex₂Braided line 129
11. lemma OAI.IntervalBar.Diagram.map_ε_app line 134
12. lemma OAI.IntervalBar.Diagram.map_η_app line 138
13. lemma OAI.IntervalBar.Diagram.map_μ_app line 148
14. lemma OAI.IntervalBar.Diagram.reindex_η_app line 152
15. lemma OAI.IntervalBar.Diagram.reindex_μ_app line 155
16. lemma OAI.IntervalBar.Diagram.reindex_map_app line 159
17. lemma OAI.IntervalBar.Diagram.map_map_app line 163
18. lemma OAI.IntervalBar.Diagram.map_obj line 168
19. lemma OAI.IntervalBar.Diagram.reindex₂_η_app line 171
20. lemma OAI.IntervalBar.Diagram.map_reindex₂_unit_app line 183
21. lemma OAI.IntervalBar.Diagram.map_reindex₂_id line 193
22. lemma OAI.IntervalBar.Diagram.map_reindex₂_comp line 242
23. def OAI.IntervalBar.Diagram.reindex₃ line 291
24. lemma OAI.IntervalBar.Diagram.reindex₃_id line 295
25. lemma OAI.IntervalBar.Diagram.reindex₃_comp line 300
26. def OAI.IntervalBar.Diagram.trisimplicial line 308