OAI/GroupTheory/SimpleAmenable/PolygonGeometry/CommonTranslatedCopies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SimpleAmenable.CommonFrame line 16
2. def OAI.SimpleAmenable.commonFrame line 23
3. def OAI.SimpleAmenable.spatialTranslate line 33
4. theorem OAI.SimpleAmenable.CommonFrame.conditional_projection line 43
5. theorem OAI.SimpleAmenable.InitialCoverSystem.commonTranslatedAlphabet_projection line 63
6. theorem OAI.SimpleAmenable.InitialCoverSystem.commonTranslatedAlphabet_independent line 81
7. def OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy line 90
8. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_projection line 95
9. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_aligned line 102