OAI/Geometry/HyperbolicGroups/DevelopmentRadial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_map_le line 17
2. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_homeomorph line 29
3. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_rebase line 36
4. lemma OAI.HyperbolicObstruction.LocalGeodesic.initial_close_dist_le line 42
5. lemma OAI.HyperbolicObstruction.LocalGeodesic.initial_intrinsicDist_le line 57
6. lemma OAI.HyperbolicObstruction.LocalGeodesic.joining_radial line 80
7. lemma OAI.HyperbolicObstruction.LocalGeodesic.developed_radial line 88