OAI/Geometry/HyperbolicGroups/OutsideComponentFilling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.isolated_outside_filling line 19

   Source documentation

   Components with no relator face are trees in genus zero even when the whole picture has unrelated closed components.

   theorem isolated_outside_filling
       (hclosed : ∀ x ∈ P.outside, P.pairing.edge x ∈ P.outside) :
       Homotopy R w [] 0 := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.Homotopy