OAI/Geometry/HyperbolicGroups/WalkClasses.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Face line 21
2. abbrev OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Vertex line 22
3. instance OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.(instance at line 23) line 23
4. instance OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.(instance at line 24) line 24
5. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.faceClass line 26
6. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.vertexClass line 27
7. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.faceClass_eq line 29
8. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.vertexClass_eq line 31
9. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.faceClass_out line 34
10. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.vertexClass_out line 35
11. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.kind_cycle line 37
12. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.faceKind line 41
13. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.faceKind_mk line 42
14. abbrev OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Link line 44
15. def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.linkNext line 46
16. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.linkNext_val line 52
17. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.link_cyclic line 54
18. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.link_card line 61