OAI/Geometry/HyperbolicGroups/ConeFanCorner.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.leftDart line 18
2. def OAI.HyperbolicObstruction.ConeSkeleton.rightDart line 19
3. def OAI.HyperbolicObstruction.ConeSkeleton.dartPart line 21
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.left_part line 26
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.right_part line 27
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.endpoints_injective line 29
7. def OAI.HyperbolicObstruction.ConeSkeleton.corner line 47
8. def OAI.HyperbolicObstruction.ConeSkeleton.cornerOut line 50
9. def OAI.HyperbolicObstruction.ConeSkeleton.cornerIn line 53
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.corner_label line 56
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.corner_previous_label line 60
12. lemma OAI.HyperbolicObstruction.ConeSkeleton.corner_start line 65
13. lemma OAI.HyperbolicObstruction.ConeSkeleton.apex_side_corner line 71

    Source documentation

    These are precisely the two orientations of the apex corner of an actual indexed fan triangle. No quotient by generator labels is made.

    lemma apex_side_corner (f : FanTriangle n w) (o : Bool) (i : Fin 3)
        (ha : isApex n w (start n w ((boundary n w d).sideLabel ⟨.inl f,o,i⟩)) = true) :
        (⟨.inl f,o,i⟩ : (boundary n w d).Side) = corner n w d f o := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.corner

14. lemma OAI.HyperbolicObstruction.ConeSkeleton.corner_bipartite line 82
15. lemma OAI.HyperbolicObstruction.ConeSkeleton.reverse_corner_unique line 93

    Source documentation

    A reversed pair of apex corner ports determines the SAME fan triangle with opposite orientation. This is the actual simple bipartite fan graph fact that rules out a triangle-only two-step link in a reduced picture.

    lemma reverse_corner_unique {f g : FanTriangle n w} {o p : Bool}
        (hout : cornerOut n w f o = cornerIn n w g p)
        (hin : cornerIn n w f o = cornerOut n w g p) : g = f ∧ p = !o := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.cornerOut, OAI.HyperbolicObstruction.ConeSkeleton.cornerIn

16. lemma OAI.HyperbolicObstruction.ConeSkeleton.reverse_corner_index line 104