OAI/Geometry/HyperbolicGroups/DevelopmentGeodesic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.LocalGeodesic.joining_length_variation line 17
2. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_joining_le line 26
3. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_to_joining line 32
4. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_joining line 36
5. def OAI.HyperbolicObstruction.LocalGeodesic.developedSegment line 44
6. lemma OAI.HyperbolicObstruction.LocalGeodesic.developedSegment_spec line 47
7. lemma OAI.HyperbolicObstruction.LocalGeodesic.developed_isGeodesic line 55
8. lemma OAI.HyperbolicObstruction.LocalGeodesic.endpoint_dist_le_intrinsic line 58
9. lemma OAI.HyperbolicObstruction.LocalGeodesic.endpoint_dist_eq_of_short line 63
10. lemma OAI.HyperbolicObstruction.LocalGeodesic.projected_localSegment line 68
11. lemma OAI.HyperbolicObstruction.LocalGeodesic.developedSegment_unique line 83