OAI/Geometry/HyperbolicGroups/WordPicturePeel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_other_boundary line 17
2. def OAI.HyperbolicObstruction.WordPictures.WordPicture.peelAt line 43

   Source documentation

   Peeling a genuine interior face adjacent to the outside deletes one paired edge and retains every other indexed relator boundary and label.

   def peelAt {a : P.Dart} {l r : List P.Dart} (he : P.outside = a::l)
       (hr : IsBoundary P.pairing.face (P.pairing.edge a::r))
       (hne : ¬ P.pairing.face.SameCycle a (P.pairing.edge a)) :
       WordPicture R ((r++l).map P.label) := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.WordPicture