OAI/Geometry/HyperbolicGroups/LocalGeodesicTopology.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.small_ball_pathConnected line 16
2. lemma OAI.HyperbolicObstruction.UniformMetricCoverData.locallyPathConnected line 47
3. lemma OAI.HyperbolicObstruction.LocalGeodesic.locallyPathConnected line 64
4. def OAI.HyperbolicObstruction.LocalGeodesic.rebaseMap line 68

   Source documentation

   The actual unique lift between based local-geodesic covers.

   def rebaseMap (a : LocalGeodesic o) : C(LocalGeodesic (endpoint a),LocalGeodesic o) := by
   …

   Mentions: OAI.HyperbolicObstruction.LocalGeodesic, OAI.HyperbolicObstruction.LocalGeodesic.endpoint

5. lemma OAI.HyperbolicObstruction.LocalGeodesic.rebaseMap_start line 73
6. lemma OAI.HyperbolicObstruction.LocalGeodesic.rebaseMap_endpoint line 77