OAI/Topology/ArtinGroups/ParabolicIntersections/TreeAvoidingGraph.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coning off paths that avoid a fixed orbit of segments

The vertices remain those of the original tree. A new edge joins the endpoints of a path containing no translate of the chosen segment.

  1. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.avoidingGraph line 17
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.avoidingGraph_subpath line 27
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.avoidingGraph_preservesAdj line 37
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.le_avoidingGraph line 59

    Source documentation

    If the chosen segment has at least two edges, every original edge remains an edge after coning.

    lemma le_avoidingGraph (hT : T.IsAcyclic) (hA : PreservesAdj (G := G) T)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj

  5. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.avoidingGraph_pathSaturated line 82
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.avoidingGraph_connected line 87