OAI/GroupTheory/SimpleAmenable/CentralCovers/FullAlphabetGeneration.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.five_alphabet_generate line 17
2. theorem OAI.SimpleAmenable.universal_five_alphabet_generate line 29
3. theorem OAI.SimpleAmenable.smallFamilyModel_surjective line 41
4. theorem OAI.SimpleAmenable.InitialCoverSystem.fullPrimitiveProjection line 53
5. def OAI.SimpleAmenable.InitialCoverSystem.fullPrimitiveTable line 64
6. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveFamily_range_full line 78
7. theorem OAI.SimpleAmenable.InitialCoverSystem.constant_range_full line 97
8. def OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector line 114
9. theorem OAI.SimpleAmenable.InitialCoverSystem.fullGeometricSector_projection line 122