TreeShortcutAcylindrical.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform acylindricity of the graph obtained by coning off segment-free paths.

theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.avoidingGraph_acylindrical_count line 15
Source documentation
The constants depend only on displacement and on the chosen free segment, even when the original tree has infinite-valence vertices.
```
theorem avoidingGraph_acylindrical_count (hT : T.IsTree)
    (hA : PreservesAdj (G := G) T) (hfree : pairStabilizer (G := G) u v=⊥)
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj, OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer