OAI/GroupTheory/SimpleAmenable/CentralCovers/RefinedClippedModels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.refined_clipped_model_action_neighborhood line 17
2. inductive OAI.SimpleAmenable.PrimitiveGerm line 93
3. theorem OAI.SimpleAmenable.PrimitiveGerm.nonempty line 105
4. def OAI.SimpleAmenable.PrimitiveGerm.Index line 119
5. instance OAI.SimpleAmenable.PrimitiveGerm.(instance at line 124) line 124
6. def OAI.SimpleAmenable.PrimitiveGerm.cuts line 127
7. def OAI.SimpleAmenable.PrimitiveGerm.oldOffset line 136
8. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.constant_model_action line 148