OAI/Geometry/HyperbolicGroups/ConeExteriorWalk.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.OutsideCellSide line 22
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkTarget line 23
3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkFrozen line 24
4. def OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellStep line 27
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellStep_label line 32
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellStep_kind line 41
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellStep_closed line 52
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellStep_frozen_next line 64
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellStep_frozen_inj line 77
10. abbrev OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellTarget line 102
11. def OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellToWalk line 109

    Source documentation

    Transfer keeps the raw diagram and arbitrary outside word literally, while opening top polygon steps to the checked cone surgeries.

    def exteriorCellToWalk : WalkPicture.{u} (exteriorWalkTarget n w d ell hell word closed c hc f) where
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkTarget

12. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellToWalk_frozen line 135
13. lemma OAI.HyperbolicObstruction.ConeSkeleton.exteriorCellToWalk_tag line 151