OAI/GroupTheory/SimpleAmenable/Simplicial/TripleComposition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntervalBar.Diagram.map_unit_component line 16
2. lemma OAI.IntervalBar.Diagram.map_cut_component line 24
3. lemma OAI.IntervalBar.Diagram.map₂_comp_obj line 30
4. lemma OAI.IntervalBar.Diagram.map₂_comp line 57
5. lemma OAI.IntervalBar.Diagram.map₃_comp_obj line 65
6. lemma OAI.IntervalBar.Diagram.map₃_comp line 119
7. lemma OAI.IntervalBar.Diagram.bar₃Map_comp line 133
8. def OAI.BarFinitePower.swap line 147
9. def OAI.BarFinitePower.swapEquiv line 150
10. instance OAI.BarFinitePower.(instance at line 159) line 159
11. def OAI.BarFinitePower.project line 163
12. instance OAI.BarFinitePower.(instance at line 164) line 164
13. def OAI.BarFinitePower.tripleProject line 165
14. lemma OAI.BarFinitePower.tripleProject_eval line 169
15. instance OAI.BarFinitePower.(instance at line 172) line 172
16. def OAI.BarFinitePower.power line 185
17. def OAI.BarFinitePower.lift line 196
18. def OAI.BarFinitePower.nervePiIso line 202
19. lemma OAI.BarFinitePower.lift_nerve line 209
20. lemma OAI.BarFinitePower.lift_nerve_homology_isIso line 211