OAI/Geometry/HyperbolicGroups/IndexedPictureExistence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Literal nullword disks with chosen persistent cell identities.

  1. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.outsideInvariant line 18
  2. abbrev OAI.HyperbolicObstruction.WordPictures.WordPicture.InsideDart line 23
  3. def OAI.HyperbolicObstruction.WordPictures.WordPicture.insideFace line 24
  4. def OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing.ofInterior line 31

    Source documentation

    Convert a coherent map on the genuine interior faces into a persistent optional index on the entire diagram.

    def Indexing.ofInterior (j : P.InsideDart → B.Side)
    (hj : IndexedFaceMap P.insideFace B.next j)
    (hl : ∀ x, P.label x.val = B.sideLabel (j x)) : Indexing B P where
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.WordPicture.Indexing

  5. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.indexing_exists line 57