OAI/Geometry/HyperbolicGroups/LocalGeodesicContraction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.LocalGeodesic.initial line 15
2. lemma OAI.HyperbolicObstruction.LocalGeodesic.prefix_apply line 19
3. lemma OAI.HyperbolicObstruction.LocalGeodesic.prefix_zero line 24
4. lemma OAI.HyperbolicObstruction.LocalGeodesic.prefix_one line 27
5. lemma OAI.HyperbolicObstruction.LocalGeodesic.endpoint_prefix line 30
6. lemma OAI.HyperbolicObstruction.LocalGeodesic.length_prefix line 32
7. lemma OAI.HyperbolicObstruction.LocalGeodesic.prefix_continuous line 36
8. def OAI.HyperbolicObstruction.LocalGeodesic.contraction line 43
9. instance OAI.HyperbolicObstruction.LocalGeodesic.(instance at line 46) line 46