RelativeFanCapacity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozenCorner_start line 22
lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.fan_field_once line 30
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 (frozen n w d ell hell word 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 = .inl (frozenCorner n w d g o))
    (hy : P.index y = .inl (frozenCorner n w d g p))
    (hxy : P.pairing.vertex.SameCycle x y) : x = y := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.frozenCorner