OAI/Geometry/HyperbolicGroups/RelativeTriangleTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.AllTriangleIndex line 29
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangleCorner line 31
3. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangleRawDart line 33
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangle_selected line 36
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangle_raw_index line 45
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangleRawDart_injective line 57
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.allTriangleIndex_card line 68
8. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTriangleFace line 75
9. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 77) line 77
10. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangleFace line 79
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangleFace_surjective line 89
12. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedTriangles_le line 127
13. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangleFace_injective line 133
14. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedTriangles_eq line 156