OAI/Geometry/HyperbolicGroups/WalkFanCapacity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.frozenCorner_start line 23
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.fan_field_once line 31

   Source documentation

   The same indexed fan field occurs at most once at one normalized apex instance, INCLUDING opposite triangle orientations. Opposite orientations would force a canceling two-step vertex link.

   lemma fan_field_once (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
       (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w))
       {x y : P.Dart} {g : FanTriangle n w} {o p : Bool}
       (hx : P.index x = frozenCorner n w d g o)
       (hy : P.index y = frozenCorner n w d g p)
       (hxy : P.pairing.vertex.SameCycle x y) : x = y := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.frozenCorner