OAI/Geometry/HyperbolicGroups/GraphSubpairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphPairing line 22

   Source documentation

   Retain all literal edge copies whose endpoints are adjacent in T. Fixed darts are stubs; no parallel edge is silently identified.

   def graphPairing (T : SimpleGraph M.GraphVertex) : Perm D :=
   …

2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphPairing_apply line 30
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphPairing_sub line 34
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphPairing_graph line 38
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_span_of_connected line 53