OAI/Geometry/HyperbolicGroups/PictureLeaf.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.cycles_le_half_of_no_fixed line 16
2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.cycles_eq_one line 34
3. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.single_face_leaf line 49

   Source documentation

   A one-face genus-zero side pairing has a genuine valence-one vertex. The genus assumption is essential: the analogous torus pairing has none.

   theorem PictureMap.single_face_leaf (M : PictureMap D) (hG : M.GenusZero)
       {xs : List D} (hb : IsBoundary M.face xs) (hall : ∀ x, x ∈ xs)
       (hne : xs ≠ []) : ∃ x, M.face (M.edge x) = x := by
   …

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