OAI/Geometry/HyperbolicGroups/IndexedPictureBasic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact cell disks, free spurs and cyclic basepoint changes with persistent cell-side identities.

  1. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.empty line 20
  2. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.empty_chain line 28
  3. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.freePair line 32
  4. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.freePair_chain line 46
  5. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.rotate line 49
  6. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.rotate_chain line 58
  7. def OAI.HyperbolicObstruction.WordPictures.WordPicture.cellDisk line 64

    Source documentation

    The literal indicated cell, not a reselected word-equivalent relator.

    def cellDisk : WordPicture (Set.range B.attachingWord) (B.attachingWord c) where
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.WordPicture

  8. def OAI.HyperbolicObstruction.WordPictures.WordPicture.cellDiskIndex line 98
  9. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.cellDisk_chain line 133