OAI/Geometry/HyperbolicGroups/LocalGeodesicLength.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.local_dist_le_global line 15
2. lemma OAI.HyperbolicObstruction.LocalGeodesic.close_length line 59
3. lemma OAI.HyperbolicObstruction.LocalGeodesic.length_continuous line 69
4. lemma OAI.HyperbolicObstruction.LocalGeodesic.length_variation line 77