OAI/Geometry/HyperbolicGroups/LocalGeodesicCover.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The space of genuine local geodesics based at a point, with its uniform function-space topology. The endpoint map is a produced covering map.

  1. lemma OAI.HyperbolicObstruction.IsLocalSegment.congr line 20
  2. def OAI.HyperbolicObstruction.LocalGeodesic.extend line 28
  3. lemma OAI.HyperbolicObstruction.LocalGeodesic.extend_coe line 29
  4. lemma OAI.HyperbolicObstruction.LocalGeodesic.extend_mem line 30
  5. lemma OAI.HyperbolicObstruction.LocalGeodesic.extend_zero line 32
  6. lemma OAI.HyperbolicObstruction.LocalGeodesic.extend_one line 33
  7. def OAI.HyperbolicObstruction.LocalGeodesic line 37
  8. instance OAI.HyperbolicObstruction.LocalGeodesic.(instance at line 41) line 41
  9. instance OAI.HyperbolicObstruction.LocalGeodesic.(instance at line 42) line 42
  10. lemma OAI.HyperbolicObstruction.LocalGeodesic.start line 44
  11. def OAI.HyperbolicObstruction.LocalGeodesic.length line 46
  12. lemma OAI.HyperbolicObstruction.LocalGeodesic.localSegment line 47
  13. lemma OAI.HyperbolicObstruction.LocalGeodesic.length_nonneg line 48
  14. def OAI.HyperbolicObstruction.LocalGeodesic.endpoint line 50
  15. lemma OAI.HyperbolicObstruction.LocalGeodesic.endpoint_lipschitz line 51
  16. lemma OAI.HyperbolicObstruction.LocalGeodesic.endpoint_continuous line 56
  17. lemma OAI.HyperbolicObstruction.LocalGeodesic.ext line 58
  18. def OAI.HyperbolicObstruction.LocalGeodesic.ofReal line 61
  19. lemma OAI.HyperbolicObstruction.LocalGeodesic.ofReal_apply line 63
  20. lemma OAI.HyperbolicObstruction.LocalGeodesic.ofReal_length line 64
  21. def OAI.HyperbolicObstruction.LocalGeodesic.constant line 69
  22. lemma OAI.HyperbolicObstruction.LocalGeodesic.constant_apply line 71
  23. instance OAI.HyperbolicObstruction.LocalGeodesic.(instance at line 72) line 72
  24. lemma OAI.HyperbolicObstruction.LocalGeodesic.close_isometry line 74
  25. lemma OAI.HyperbolicObstruction.LocalGeodesic.short_lift line 85
  26. lemma OAI.HyperbolicObstruction.LocalGeodesic.coverData line 107
  27. lemma OAI.HyperbolicObstruction.LocalGeodesic.isCoveringMap line 111