OAI/GroupTheory/SimpleAmenable/CentralCovers/UniformTangentTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SimpleAmenable.InitialCoverSystem.tangent_transport_uniform line 19
2. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentChartSector_eq_containing_window line 78
3. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_supported line 114
4. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_control_from_rectangle line 125