OAI/Geometry/HyperbolicGroups/PrismConcat.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous concatenation of literal prisms, with pointwise restriction identities. No change in the endpoint maps is hidden by homotopy classes.

  1. def OAI.HyperbolicObstruction.PrismConcat.endpoint line 15
  2. def OAI.HyperbolicObstruction.PrismConcat.homotopy line 16
  3. def OAI.HyperbolicObstruction.PrismConcat.continuation line 21
  4. def OAI.HyperbolicObstruction.PrismConcat.concat line 27
  5. lemma OAI.HyperbolicObstruction.PrismConcat.initial line 30
  6. lemma OAI.HyperbolicObstruction.PrismConcat.final line 34
  7. lemma OAI.HyperbolicObstruction.PrismConcat.agree line 39
  8. lemma OAI.HyperbolicObstruction.PrismConcat.constant_at line 49