OAI/Geometry/HyperbolicGroups/EdgeErase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_invariant line 17
2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge line 29

   Source documentation

   Deletion of an actual paired edge: its incident face boundaries are spliced and the two indexed sides erased. No label or surface premise is hidden in this finite permutation construction.

   def eraseEdge : PictureMap {x // OffPair a (M.edge a) x} where
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.OffPair

3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_vertex line 36
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_face_orbits line 50
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_vertex_perm line 56