OAI/Geometry/HyperbolicGroups/EdgeEraseGenus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_euler line 19
2. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_genusZero line 52

   Source documentation

   Deleting an edge separating two distinct face cycles preserves actual combinatorial genus zero, including the component consisting of two monogons.

   theorem eraseEdge_genusZero (hG : M.GenusZero)
       (hne : ¬ M.face.SameCycle a (M.edge a)) : (M.eraseEdge a).GenusZero := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero