OAI/Geometry/HyperbolicGroups/PathInSet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Endpoint-preserving restrictions and homotopies inside a simply connected subspace. Used to turn coordinate-star homotopies into actual path homotopies.

  1. def OAI.HyperbolicObstruction.PathInSet.restrict line 13
  2. lemma OAI.HyperbolicObstruction.PathInSet.restrict_map line 20
  3. lemma OAI.HyperbolicObstruction.PathInSet.homotopic line 23