OAI/GroupTheory/SimpleAmenable/CentralCovers/ConcurrentCoordinateGates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.concurrentCoordinateEmbedding line 20
2. def OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.concurrentCoordinates line 25
3. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.concurrentCoordinates_eq line 29
4. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.coordinate_margin_resolved line 39
5. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.coordinate_positive_resolved line 51
6. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.coordinate_inward_resolved line 59
7. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.coordinate_localDecision_resolved line 73
8. theorem OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas.coordinate_control_inward_gate line 84