OAI/GroupTheory/SimpleAmenable/PolygonGeometry/CanonicalSectors.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.perfect_maps_commute_of_central line 17
2. theorem OAI.SimpleAmenable.perfect_finite_pi line 37
3. def OAI.SimpleAmenable.sectorMask line 50
4. theorem OAI.SimpleAmenable.sectorMask_of_mem line 56
5. theorem OAI.SimpleAmenable.sectorMask_of_not_mem line 61
6. theorem OAI.SimpleAmenable.sectorMask_commute line 66
7. theorem OAI.SimpleAmenable.sectorMask_disjoint_union line 74
8. def OAI.SimpleAmenable.centralSector line 83
9. theorem OAI.SimpleAmenable.centralSector_spec line 89
10. theorem OAI.SimpleAmenable.centralSector_commute line 97
11. def OAI.SimpleAmenable.commutingProduct line 106
12. theorem OAI.SimpleAmenable.commutingProduct_apply line 110
13. theorem OAI.SimpleAmenable.centralSector_union line 114
14. theorem OAI.SimpleAmenable.centralSector_empty line 127
15. theorem OAI.SimpleAmenable.centralSector_trivial line 136
16. def OAI.SimpleAmenable.assignmentPullback line 145
17. theorem OAI.SimpleAmenable.centralSector_refine line 150
18. def OAI.SimpleAmenable.centralSectorProduct line 159
19. theorem OAI.SimpleAmenable.centralSectorProduct_single line 164
20. def OAI.SimpleAmenable.assignmentProjection line 170
21. theorem OAI.SimpleAmenable.assignmentProjection_surjective line 175
22. theorem OAI.SimpleAmenable.centralSectorProduct_spec line 181
23. theorem OAI.SimpleAmenable.centralSectorProduct_surjective line 196
24. theorem OAI.SimpleAmenable.centralSector_generate line 208