OAI/GroupTheory/SimpleAmenable/Simplicial/StageNerveColimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StageNerveColimit.comp_injective line 12
2. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.nerveCocone line 23
3. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.nerveIsColimit line 25
4. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusionMonoidal line 44
5. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusionBraided line 69
6. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion_η line 75
7. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion_ε line 76
8. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion_μ line 77
9. lemma OAI.IntervalBar.Diagram.map_obj_injective line 86
10. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map_inclusion_id line 125
11. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map_inclusion_comp line 136
12. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.map_inclusion_forget line 149
13. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.barStage line 162
14. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.barCocone line 167
15. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.barNerveCocone line 172
16. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.barNerveIsColimit line 174