OAI/Geometry/HyperbolicGroups/FaceSplit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_le_glue_splice line 18
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.split_components_glue line 33
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.split_components_card line 41
  4. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.split_genusZero line 53

    Source documentation

    Split a face at ANY two of its corners, identifying their endpoint regions. Neither an embedded boundary nor distinct source endpoints is required. If the endpoints were already equal the affected sphere can split into two; otherwise the number of components is unchanged.

    theorem split_genusZero (hM : M.GenusZero) (a b : D)
    (hne : a ≠ b) (hf : M.face.SameCycle a b) : (M.splice a b).GenusZero := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero