OAI/Geometry/HyperbolicGroups/LocalGeodesicRebase.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.LocalGeodesic.basedLift line 17
  2. lemma OAI.HyperbolicObstruction.LocalGeodesic.basedLift_start line 23
  3. lemma OAI.HyperbolicObstruction.LocalGeodesic.basedLift_endpoint line 29
  4. lemma OAI.HyperbolicObstruction.LocalGeodesic.basedLift_inv line 35
  5. def OAI.HyperbolicObstruction.LocalGeodesic.basedHomeomorph line 45

    Source documentation

    Re-basing changes the genuine local-geodesic model by a covering isomorphism.

    def basedHomeomorph (a : LocalGeodesic o) (b : LocalGeodesic q) (he : endpoint b=endpoint a) :
    LocalGeodesic o ≃ₜ LocalGeodesic q where
…

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

  6. def OAI.HyperbolicObstruction.LocalGeodesic.rebase line 54
  7. lemma OAI.HyperbolicObstruction.LocalGeodesic.rebase_start line 57
  8. lemma OAI.HyperbolicObstruction.LocalGeodesic.rebase_endpoint line 59
  9. lemma OAI.HyperbolicObstruction.LocalGeodesic.rebase_symm_endpoint line 61
  10. lemma OAI.HyperbolicObstruction.LocalGeodesic.rebase_symm_self line 63