OAI/Geometry/HyperbolicGroups/WordPictureAppend.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.splice_nonempty line 19
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.splice_away line 27
  3. def OAI.HyperbolicObstruction.WordPictures.WordPicture.appendNonempty line 46

    Source documentation

    Literal concatenation by a genus-zero connected sum at exterior corners.

    def appendNonempty (hp : P.outside ≠ []) (hq : Q.outside ≠ []) : WordPicture R (u++v) where
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.WordPicture

  4. def OAI.HyperbolicObstruction.WordPictures.WordPicture.append line 94