OAI/Topology/ArtinGroups/ParabolicIntersections/TreePaths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Elementary path geometry in a simplicial tree.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.common_support_eq_start line 11

    Source documentation

    Paths starting in different directions meet only at their initial vertex.

    theorem common_support_eq_start (hT : T.IsAcyclic) {u v w x : V}
    (p : T.Walk u v) (q : T.Walk u w) (hp : p.IsPath) (hq : q.IsPath)
    (hs : p.snd≠q.snd) (hxp : x∈p.support) (hxq : x∈q.support) : x=u := by
…
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.reverse_append_isPath line 23

    Source documentation

    Two paths in different directions form a single longer path.

    theorem reverse_append_isPath (hT : T.IsAcyclic) {u v w : V}
    (p : T.Walk u v) (q : T.Walk u w) (hp : p.IsPath) (hq : q.IsPath)
    (hs : p.snd≠q.snd) : (p.reverse.append q).IsPath := by
…