IndexedBoundaryPullback.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap.pullback_boundary line 16
Source documentation
An indexed face map pulls back a complete target polygon to exactly one source face, without any injectivity assumption on target letter labels.
```
theorem IndexedFaceMap.pullback_boundary {f : Perm D} {t : Perm S} {j : D → S}
    (h : IndexedFaceMap f t j) (a : D) {ys : List S}
    (ht : IsBoundary t ys) (ha : j a ∈ ys) :
    ∃ xs : List D, IsBoundary f xs ∧ a ∈ xs ∧ xs.map j = ys := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap, OAI.HyperbolicObstruction.PictureSwitch.IsBoundary