OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FinePatchAtlas.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.ConcurrentGeometry.refineMesh line 18
2. theorem OAI.SimpleAmenable.ConcurrentGeometry.exists_finer line 29
3. theorem OAI.SimpleAmenable.rectangularAtlas_fixed_radius_eventually line 44
4. structure OAI.SimpleAmenable.InitialCoverSystem.FinePatchAtlas line 70
5. theorem OAI.SimpleAmenable.finePatchAtlas_eventually line 75
6. theorem OAI.SimpleAmenable.cutForm_dist_bound line 101
7. theorem OAI.SimpleAmenable.windowRectangle_far_sign line 121
8. theorem OAI.SimpleAmenable.windowRectangle_far_clipped line 145