OAI/Geometry/HyperbolicGroups/BoundaryRotation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.rotate_append line 14
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.adjacent_rotate line 18
  3. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.rotate_null line 41

    Source documentation

    Moving the boundary basepoint is area-free for a null word; it is not asserted that a cyclic shift represents the same free-group element.

    lemma rotate_null (h : Homotopy R (v++u) [] k) : Homotopy R (u++v) [] k := by
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.Homotopy

  4. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.unrotate_null line 46
  5. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.all_outside_rotate line 57
  6. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.all_outside_fold line 60