OAI/Geometry/HyperbolicGroups/GeometricSpaceTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Isometric transport of the literal CAT(0) comparison and geometric actions, including the universe lift required by the unchanged main statement.

  1. lemma OAI.HyperbolicObstruction.CATZero.of_isometryEquiv line 17
  2. def OAI.HyperbolicObstruction.GeometricAction.spaceTransport line 35
  3. def OAI.HyperbolicObstruction.uliftIsometry line 63
  4. lemma OAI.HyperbolicObstruction.ulift_proper line 67