OAI/GroupTheory/SimpleAmenable/Configurations/StageRealization.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PolygonObject.LabelledStage.realizeObject line 18
2. def OAI.SimpleAmenable.PolygonObject.LabelledStage.realize line 25
3. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.labelIndex line 33
4. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.labelIndex_spec line 35
5. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.labelIndex_fiber line 40
6. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.evaluated line 43
7. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.fiberIndex line 45
8. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.trackFiber line 50
9. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sourceAtom line 53
10. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sample line 56
11. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sourceIndex line 61
12. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sourceIndex_atom line 65
13. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.sourceIndex_track line 70
14. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.reconstructMap line 77
15. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.reconstructInverse line 86
16. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.reconstruct_right line 93
17. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.reconstruct_left line 101
18. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.reconstructEquiv line 125
19. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.reconstruct line 150
20. theorem OAI.SimpleAmenable.PolygonObject.LabelledStage.realize_essSurj line 162
21. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.realize_faithful line 165
22. def OAI.SimpleAmenable.PolygonObject.LabelledStage.fiberPoint line 168
23. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.fiber_base line 177
24. def OAI.SimpleAmenable.PolygonObject.LabelledStage.fiberFin line 188
25. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.fiberFin_spec line 192
26. def OAI.SimpleAmenable.PolygonObject.LabelledStage.fiberEquiv line 199
27. def OAI.SimpleAmenable.PolygonObject.LabelledStage.fromUniform line 217
28. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.fromUniform_spec line 222
29. theorem OAI.SimpleAmenable.PolygonObject.LabelledStage.realize_full line 233
30. def OAI.SimpleAmenable.PolygonObject.LabelledStage.equivalence line 255