PictureFaceCorners.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.faceCorners_card_le_fiber line 19
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.faceCorners_card_le line 30
Source documentation
A bound on the literal side-degree of each face bounds the number of its distinct corner vertices, even for faces touching the same vertex repeatedly or traversing both sides of a loop.
```
theorem faceCorners_card_le (k : ℕ)
    (hdegree : ∀ x : D, Fintype.card {y : D // M.face.SameCycle x y} ≤ k)
    (f : M.dual.GraphVertex) : (M.faceCorners f).card ≤ k := by
…
```