OAI/Geometry/HyperbolicGroups/CompactLocalCATGeometric.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact locally CAT(-1) geodesic metrics yield genuine geometric CAT(0) actions of the actual fundamental group.

  1. lemma OAI.HyperbolicObstruction.not_noGeometricCATZeroAction_of_compact_localCATNegOne line 19
  2. lemma OAI.HyperbolicObstruction.incompatibleLocalCATNegOne_of_noAction line 38
  3. lemma OAI.HyperbolicObstruction.homotopy_incompatibleLocalCATNegOne line 56