OAI/Geometry/HyperbolicGroups/WordSubstitution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.WordPictures.substitute_reverse line 17
2. lemma OAI.HyperbolicObstruction.WordPictures.substitute_free_step line 27
3. lemma OAI.HyperbolicObstruction.WordPictures.Move.substitute line 41
4. theorem OAI.HyperbolicObstruction.WordPictures.Homotopy.substitute line 63

   Source documentation

   Quantitative substitution of proved literal relator disks. All contexts, free folds, reverse relators and intermediate words are retained.

   theorem substitute {z t : Word A} (h : Homotopy R z t k) :
       ∃ a ≤ C * k, Homotopy S (z.flatMap c) (t.flatMap c) a := by
   …

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