OAI/Geometry/HyperbolicGroups/OneFaceFilling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.one_face_filling line 17

   Source documentation

   Base case of planar extraction, proved from the combinatorial Euler definition: a genus-zero picture with no interior darts has a zero-area word filling. It is NOT postulated as a property of a picture.

   theorem one_face_filling {w : Word A} (P : WordPicture R w) (hall : ∀ x, x ∈ P.outside) :
       Homotopy R w [] 0 := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.WordPicture, OAI.HyperbolicObstruction.WordPictures.Homotopy