OAI/Geometry/HyperbolicGroups/BoundaryEraseList.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.bypassPair_consecutive line 17
2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.lift line 31
3. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.middle_next line 47
4. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.middle_offpair line 54
5. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.erase_middle line 65
6. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold_boundary line 96

   Source documentation

   The free fold deletes exactly the two consecutive entries of the literal outside word; no cyclic rotation or word-equality surrogate is used.

   theorem boundaryFold_boundary (h : IsBoundary M.face (l++a::b::r)) (hab : a ≠ b) :
       IsBoundary (M.boundaryFold hab h.middle_next).face
         ((l++r).attachWith (OffPair a b) (IsBoundary.middle_offpair h.nodup)) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary, OAI.HyperbolicObstruction.PictureSwitch.OffPair, OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.middle_offpair