GraphSubstitution.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.GraphWordFilling.word_reverse line 15
def OAI.HyperbolicObstruction.GraphWordFilling.expand line 26
Source documentation
Replace each oriented edge by a prescribed genuine edge-path. Endpoints are enforced in the type, thereby preserving closedness exactly.
```
def expand (f : V → W) (r : ∀ {u v}, G.Adj u v → H.Walk (f u) (f v)) :
    {u v : V} → G.Walk u v → H.Walk (f u) (f v)
  | _,_,.nil => .nil
  | _,_,.cons h p => (r h).append (expand f r p)
```
lemma OAI.HyperbolicObstruction.GraphWordFilling.expand_length line 31
lemma OAI.HyperbolicObstruction.GraphWordFilling.expand_word line 40