OAI/Geometry/HyperbolicGroups/DevelopmentDeck.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.LocalGeodesic.deckSubgroup line 14
2. abbrev OAI.HyperbolicObstruction.LocalGeodesic.Deck line 25
3. instance OAI.HyperbolicObstruction.LocalGeodesic.(instance at line 27) line 27
4. lemma OAI.HyperbolicObstruction.LocalGeodesic.deck_endpoint line 32
5. instance OAI.HyperbolicObstruction.LocalGeodesic.(instance at line 33) line 33
6. lemma OAI.HyperbolicObstruction.LocalGeodesic.deck_ext line 39
7. lemma OAI.HyperbolicObstruction.LocalGeodesic.deck_exists line 45
8. lemma OAI.HyperbolicObstruction.LocalGeodesic.endpoint_surjective line 50
9. lemma OAI.HyperbolicObstruction.LocalGeodesic.deck_quotientCovering line 54
10. def OAI.HyperbolicObstruction.LocalGeodesic.deckIsometry line 80
11. def OAI.HyperbolicObstruction.LocalGeodesic.deckIsometricAction line 89
12. def OAI.HyperbolicObstruction.LocalGeodesic.deckPiOneEquiv line 99