OAI/GroupTheory/SimpleAmenable/Configurations/CellFiber.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PolygonObject.Labelled.Cell.fiber line 21
2. lemma OAI.SimpleAmenable.PolygonObject.Labelled.Cell.fiber_natural line 27
3. def OAI.SimpleAmenable.PolygonObject.Labelled.Cell.evaluationIso line 30
4. lemma OAI.SimpleAmenable.PolygonObject.Labelled.Cell.evaluationIso_apply line 40
5. lemma OAI.SimpleAmenable.PolygonObject.Labelled.Cell.fiber_sum_left line 43
6. lemma OAI.SimpleAmenable.PolygonObject.Labelled.Cell.fiber_sum_right line 47
7. instance OAI.SimpleAmenable.PolygonObject.Labelled.Cell.evaluationIsoMonoidal line 51
8. lemma OAI.SimpleAmenable.PolygonObject.Labelled.Cell.fiber_empty line 68
9. lemma OAI.SimpleAmenable.PolygonObject.Labelled.Cell.empty_size line 71
10. def OAI.SimpleAmenable.PolygonObject.Labelled.Cell.emptyIso line 75
11. instance OAI.SimpleAmenable.PolygonObject.Labelled.Cell.emptyIsoMonoidal line 81
12. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointFiber line 99
13. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointFiber_natural line 112
14. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointEvaluationIso line 123
15. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointFiber_sum_inl line 142
16. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointFiber_sum_inr line 145
17. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointEvaluationIso_enum line 148
18. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointEvaluationIso_monoidal line 155
19. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.pointFiber_empty_of_new_label line 180
20. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.point_new_label_size line 185
21. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.emptyPointIso line 189
22. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.emptyPointIsoMonoidal line 195