OAI/Geometry/HyperbolicGroups/WordPictureArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.cycles_positive line 16
2. theorem OAI.HyperbolicObstruction.WordPictures.WordPicture.filling_interior line 24

   Source documentation

   The distinguished outside is not paid for: a nonempty literal boundary has a filling costing at most the number of INTERIOR face cycles.

   theorem filling_interior {w : Word A} (P : WordPicture R w) (ho : P.outside ≠ []) :
       ∃ n, Homotopy R w [] n ∧ n ≤ Fintype.card P.Dart / 2 ∧
         (n : ℤ) + 1 ≤ cycles P.pairing.face := by
   …

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