EdgeEraseComponents.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_components_le line 18
Source documentation
When the spliced face retains a side, deleting its paired edge cannot create a new component. This is a quotient-of-darts proof, not a drawing.
```
lemma eraseEdge_components_le (c : {x // OffPair a (M.edge a) x})
    (ha : (M.face * swap a (M.edge a)).SameCycle a c.val)
    (hb : (M.face * swap a (M.edge a)).SameCycle (M.edge a) c.val) :
    Nat.card (Quotient (M.eraseEdge a).components) ≤ Nat.card (Quotient M.components) := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.OffPair, OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_component_witness line 84