OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FiniteRefiningGrid.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.finite_refining_grid line 15
2. theorem OAI.SimpleAmenable.finite_grid_no_between line 73
3. theorem OAI.SimpleAmenable.finite_grid_refines_window line 85
4. theorem OAI.SimpleAmenable.coordinateInterval_mem_preferred line 108
5. def OAI.SimpleAmenable.refinedGridRectangle line 126
6. theorem OAI.SimpleAmenable.refinedGridRectangle_mem line 130
7. theorem OAI.SimpleAmenable.refinedGridRectangle_cover line 144
8. theorem OAI.SimpleAmenable.refinedGridRectangle_disjoint line 156
9. theorem OAI.SimpleAmenable.refinedGridRectangle_resolved line 173