OAI/GroupTheory/SimpleAmenable/PolygonGeometry/UniformPropagationBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.conjugate_eq_label line 15
2. theorem OAI.SimpleAmenable.contracted_transverse_label line 20
3. theorem OAI.SimpleAmenable.tangent_displacement_embeddings line 41
4. theorem OAI.SimpleAmenable.tangent_chain_uniform line 64
5. theorem OAI.SimpleAmenable.short_window_scale line 131
6. theorem OAI.SimpleAmenable.short_window_path line 149
7. theorem OAI.SimpleAmenable.old_window_bridge_geometry line 168