OAI/Geometry/HyperbolicGroups/GeneralSwitch.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_opposite line 19
2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_edge_a_of_ne line 25
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_edge_b_of_ne line 29
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex_switch_order line 33
5. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_genusZero_general line 57

   Source documentation

   Genus-zero is preserved by ANY cross-pairing of two outgoing edges at a single actual source vertex, even when some far vertex is the same source vertex. This includes the switches used in elementary disk cancellation. The radial case is the disjoint-far-vertices special case.

   theorem switch_genusZero_general (hM : M.GenusZero) (a b : D)
       (hv : M.vertex.SameCycle a b) : (M.switch a b).GenusZero := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero