RelativeMacroPolygon.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.mappedMacroPolygon line 26
Source documentation
The actual simple macro polygon carried by one free source face. Its vertices are the original TEMPLATE vertices in their original cyclic order, not the possibly identified letter-bouquet vertices. This supplies the finite macro-cycle perimeter/three-fan bounds from the produced normal picture.
```
noncomputable def mappedMacroPolygon (hs : P.Simple) (hb : P.NoBigon)
    (x : P.Dart) (a : Top n w) (e : MacroGraph.graph.Dart) (hx : P.index x = .inl (.inl (a,e))) :
    MacroGraph.Polygon := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.MacroGraph.Polygon