OAI/GroupTheory/SimpleAmenable/PolygonGeometry/CoordinateModels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SimpleAmenable.CoordinateGerm line 11
2. theorem OAI.SimpleAmenable.coordinateGerm_nonempty line 20
3. def OAI.SimpleAmenable.CoordinateGerm.lower line 27
4. def OAI.SimpleAmenable.CoordinateGerm.upper line 28
5. theorem OAI.SimpleAmenable.CoordinateGerm.model_formula line 30
6. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.coordinate_model_action_neighborhood line 65
7. theorem OAI.SimpleAmenable.ClippedGerm.inactive_model_restrict_gate line 137
8. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.inactive_clipped_model_action_neighborhood line 174