OAI/Geometry/HyperbolicGroups/RelativeApexLocal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.target line 22
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen line 24
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.start_link_constant line 28
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.apex_interior line 34
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.index_edge_previous line 44
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.corner_previous line 55
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.corner_reverse line 58
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.corner_label line 61
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.corner_ports line 65
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.corner_no_two_step line 77
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fan_corner line 89
12. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.apex_cases line 97
13. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.top_adjacent_different line 133
14. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.top_unique_turn line 156
15. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.apex_no_fixed line 175
16. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.link_card line 184
17. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.vertex_inverse line 199
18. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.corner_incoming line 206
19. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangle_bipartite line 216
20. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.triangle_inverse_no_two line 224