OAI/Geometry/HyperbolicGroups/LocalGeodesicDistance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.LocalGeodesic.constant_length line 20
2. lemma OAI.HyperbolicObstruction.LocalGeodesic.eq_constant_of_length_zero line 23
3. def OAI.HyperbolicObstruction.LocalGeodesic.joining line 29
4. lemma OAI.HyperbolicObstruction.LocalGeodesic.joining_zero line 33
5. lemma OAI.HyperbolicObstruction.LocalGeodesic.joining_one line 35
6. lemma OAI.HyperbolicObstruction.LocalGeodesic.joining_endpoint line 37
7. def OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist line 41
8. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_nonneg line 42
9. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_self line 43
10. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_eq_zero line 44
11. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_variation line 49
12. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_comm line 57
13. lemma OAI.HyperbolicObstruction.LocalGeodesic.intrinsicDist_triangle line 63
14. lemma OAI.HyperbolicObstruction.LocalGeodesic.ordinary_dist_le_intrinsic line 70