TreeBranch.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Reflecting a segment at an endpoint and extending it along a new edge.

lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.moved_first_vertex_ne_endpoint line 12
theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.reflected_pair line 19
Source documentation
Reflecting a path across its initial vertex intersects its endpoint stabilizer with a conjugate, and still gives an endpoint stabilizer.
```
theorem reflected_pair (u v : V) (p : T.Walk v u) (hp : p.IsPath)
    (g : G) (hg : g • v=v) (hw : g • p.snd≠p.snd) :
    pairStabilizer (G := G) u (g • u)=pairStabilizer (G := G) u v ⊓
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer
lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.reverse_concat_isPath line 50
Source documentation
An edge leaving the initial direction of a path extends the path.
```
lemma reverse_concat_isPath {u v w : V} (p : T.Walk v u) (hp : p.IsPath)
    (hadj : T.Adj v w) (hw : w≠p.snd) : (p.reverse.concat hadj).IsPath := by
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.extended_pair line 58
Source documentation
If the old stabilizer fixes the added vertex, extension preserves it.
```
theorem extended_pair (u v w : V) (p : T.Walk v u) (hp : p.IsPath)
    (hadj : T.Adj v w) (hw : w≠p.snd)
    (hfix : pairStabilizer (G := G) u v≤MulAction.stabilizer G w) :
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer