OAI/Geometry/HyperbolicGroups/LocalSegmentContinuation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.UniformLocalCATZero.mono line 16
2. theorem OAI.HyperbolicObstruction.IsLocalSegment.continuation line 22

   Source documentation

   Uniform endpoint continuation of every actual local metric geodesic.

   theorem IsLocalSegment.continuation {α : ℝ → X} {A r : ℝ}
       (hα : IsLocalSegment α A) (hr : 0<r) (hc : UniformLocalCATZero (X:=X) r)
   …

   Mentions: OAI.HyperbolicObstruction.IsLocalSegment, OAI.HyperbolicObstruction.UniformLocalCATZero