OAI/GroupTheory/SimpleAmenable/CentralCovers/CommonFrameTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.InitialCoverSystem.geometricFrameGroup line 17
2. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricFrameGroup_central line 22
3. theorem OAI.SimpleAmenable.InitialCoverSystem.frameStar_mem_geometricFrameGroup line 27
4. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_mem_geometricFrameGroup line 36
5. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_common_frame_transport line 43
6. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_common_frame_fixer line 77
7. theorem OAI.SimpleAmenable.InitialCoverSystem.frameStar_uniform line 93
8. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_uniform_mem line 106
9. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_uniform_fixer line 123
10. theorem OAI.SimpleAmenable.InitialCoverSystem.frameStar_alphabet_mem line 148