OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ChartBoundaryEndpoints.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.squareBoundaryCuts line 15
2. theorem OAI.SimpleAmenable.interval_endpoints_closed line 17
3. theorem OAI.SimpleAmenable.squareBoundaryCuts_of_closed_not_open line 24
4. theorem OAI.SimpleAmenable.squareBoundaryCuts_nonzero_on_interior line 38
5. theorem OAI.SimpleAmenable.barrier_geometric_endpoint_cut line 48
6. theorem OAI.SimpleAmenable.chart_line_endpoints_forced line 73