OAI/Geometry/HyperbolicGroups/BoundaryGraphWalk.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.graph_chain line 19
2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.graph_closed_walk line 32

   Source documentation

   Read a literal permutation face as an actual graph closed walk.

   lemma IsBoundary.graph_closed_walk (hne : xs ≠ []) :
       ∃ (v : V) (q : G.Walk v v), q.darts = xs.map j := by
   …