OAI/GroupTheory/SimpleAmenable/PolygonGeometry/LocalClippedBoxFormula.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.local_clipped_formula_with_box line 12
2. def OAI.SimpleAmenable.ClippedGerm.BoxValid line 80
3. theorem OAI.SimpleAmenable.clippedGerm_exists_box_valid line 88
4. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.decisions_locally_eq line 101
5. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.refined_coordinate_phase line 116
6. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.refined_interior_phase_bounds line 147