OAI/Geometry/HyperbolicGroups/WalkTriangleTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.AllTriangleIndex line 25
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.triangleCorner line 27
3. def OAI.HyperbolicObstruction.ConeSkeleton.triangleRawDart line 29
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.triangle_selected line 32
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.triangle_raw_index line 41
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.triangleRawDart_injective line 53
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.allTriangleIndex_card line 64
8. abbrev OAI.HyperbolicObstruction.ConeSkeleton.SelectedTriangleFace line 71
9. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 73) line 73
10. def OAI.HyperbolicObstruction.ConeSkeleton.triangleFace line 75
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.triangleFace_surjective line 85
12. lemma OAI.HyperbolicObstruction.ConeSkeleton.selectedTriangles_le line 118
13. lemma OAI.HyperbolicObstruction.ConeSkeleton.triangleFace_injective line 124
14. lemma OAI.HyperbolicObstruction.ConeSkeleton.selectedTriangles_eq line 145