OAI/GroupTheory/SimpleAmenable/CentralCovers/SmallFamilyGlobal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.centralOn_range_iff_hasCentralLaw line 17
2. theorem OAI.SimpleAmenable.smallFamily_centralOn line 41
3. theorem OAI.SimpleAmenable.exists_alphabet_balance line 87
4. def OAI.SimpleAmenable.smallAlphabetBalance line 96
5. theorem OAI.SimpleAmenable.smallAlphabetBalance_notMem line 100
6. def OAI.SimpleAmenable.InitialCoverSystem.smallPrimitiveInputs line 109
7. def OAI.SimpleAmenable.InitialCoverSystem.smallPrimitiveCarrier line 116
8. theorem OAI.SimpleAmenable.InitialCoverSystem.smallPrimitiveInputs_projection line 124
9. theorem OAI.SimpleAmenable.InitialCoverSystem.smallPrimitiveInputs_local line 137
10. theorem OAI.SimpleAmenable.InitialCoverSystem.fullPrimitiveFamily_central line 149