OAI/Geometry/HyperbolicGroups/WordPictureMarked.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.cellular_index_tag line 27

   Source documentation

   Coherent indexing retains a distinguished face tag. In particular the outside can only map to the positive exterior polygon; no opposite exterior face or extra exterior face is silently introduced.

   theorem cellular_index_tag (tag : S → K) (inside outside : K)
       (hR : ∀ r ∈ R, ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = r ∧
         (∀ y ∈ ys, tag y = inside ∧ tag (T.opposite y) = inside))
       (hw : ∃ ys : List S, IsBoundary T.next ys ∧ ys.map T.edge = w ∧
         (∀ y ∈ ys, tag y = outside)) :
       ∃ j : P.Dart → S, IndexedFaceMap P.pairing.face T.next j ∧
         (∀ x, T.edge (j x) = P.label x) ∧
         ∀ x, tag (j x) = if x ∈ P.outside then outside else inside := by
   …