OAI/GroupTheory/SimpleAmenable/PolygonGeometry/LabelShiftedCharts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.pointCoordinate line 16
2. def OAI.SimpleAmenable.pointLabel line 19
3. theorem OAI.SimpleAmenable.pointCoordinate_add line 21
4. theorem OAI.SimpleAmenable.pointLabel_add line 25
5. theorem OAI.SimpleAmenable.endpointLabel_int_mul_tau line 29
6. theorem OAI.SimpleAmenable.coordinateWindow_pointLabel line 32
7. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentChartSector_eq_window line 43