OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FiniteArrangementGerms.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.exists_interval_avoiding_countable line 14
2. theorem OAI.SimpleAmenable.avoidsCuts_rectangle line 21
3. theorem OAI.SimpleAmenable.avoidsCuts_dense line 53
4. theorem OAI.SimpleAmenable.cutForm_smul line 62
5. def OAI.SimpleAmenable.strictLineCell line 66
6. theorem OAI.SimpleAmenable.strictLineCell_open line 70
7. theorem OAI.SimpleAmenable.finite_arrangement_germ line 83