OAI/GroupTheory/SimpleAmenable/Configurations/StageOrder.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PolygonObject.BooleanPartition.Refines line 16
2. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.refines_refl line 18
3. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.refines_trans line 19
4. def OAI.SimpleAmenable.PolygonObject.BooleanPartition.join line 21
5. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.le_join_left line 23
6. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.le_join_right line 27
7. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.ReducedLabel line 33
8. structure OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage line 34
9. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.empty line 39
10. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.(instance at line 40) line 40
11. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.(instance at line 41) line 41
12. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.sup line 45
13. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.le_sup_left line 47
14. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.le_sup_right line 49
15. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.(instance at line 51) line 51
16. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.(instance at line 53) line 53
17. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.L line 54
18. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.L_reduced line 56
19. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.L_injective line 58
20. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.label_mem line 62
21. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.Obj line 72
22. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion line 73
23. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion_id line 82
24. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion_comp line 86
25. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.diagram line 91
26. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.forget line 108
27. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.forget_ε line 109
28. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.forget_η line 110
29. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.forget_μ line 111
30. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.forget_injective line 112
31. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.inclusion_forget line 114
32. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.cocone line 115
33. theorem OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.exists_lift_family line 121
34. theorem OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.exists_lift line 134
35. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.liftDiagram line 156
36. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.liftDiagram_map line 166