OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedTripleMaps.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RestrictedNerve.diagram_map_obj line 14
2. lemma OAI.RestrictedNerve.map₂_reindex_unit_app line 19
3. lemma OAI.RestrictedNerve.map₂_reindex_cut_app line 30
4. lemma OAI.RestrictedNerve.map₃_reindex_unit_app line 38
5. lemma OAI.RestrictedNerve.map₃_reindex_cut_app line 50
6. lemma OAI.RestrictedNerve.map₂_strings_reindex_id line 59
7. lemma OAI.RestrictedNerve.map₂_strings_reindex_comp line 96
8. lemma OAI.RestrictedNerve.map₃_strings_reindex_id line 136
9. lemma OAI.RestrictedNerve.map₃_reindex_comp_cut_app line 182
10. lemma OAI.RestrictedNerve.map₃_strings_reindex_comp_obj line 203
11. lemma OAI.RestrictedNerve.map₃_strings_reindex_comp line 243
12. lemma OAI.RestrictedNerve.bar₃Map_strings_reindex_id line 269
13. lemma OAI.RestrictedNerve.bar₃Map_strings_reindex_comp line 274
14. def OAI.RestrictedNerve.tripleHorizontal line 280