BraidRestriction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive braid derivations restrict to a full subdiagram.

lemma OAI.HarmonicArtin.ParabolicIntersections.positive_cons line 15
Distinct definitions of this name: OAI/Topology/ArtinGroups/ParabolicIntersections/FoldingHead.lean:21 (different declaration text). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.positive_cons@path.
theorem OAI.HarmonicArtin.ParabolicIntersections.positiveBraidRel_restrict line 21
Source documentation
No braid move can introduce a vertex outside the original support. Inside a full subdiagram every move is a defining positive Artin relation.
```
theorem positiveBraidRel_restrict [Nonempty S] {v w : List V}
    (h : PositiveBraidRel Q v w) (hv : ∀ x ∈ v, x ∈ Set.range f) :
    wordPositive N (v.map (Function.invFun f)) =
      wordPositive N (w.map (Function.invFun f)) := by
…
```
Mentions: OAI.HarmonicArtin.wordPositive