OAI/Topology/ArtinGroups/ParabolicIntersections/TreeTripod.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.walk_common_prefix line 11
2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.tree_tripod line 32
3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.prefixes_comparable line 56
4. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.common_support_in_prefix line 70
5. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.tree_branchpoint line 87

   Source documentation

   The common prefix contains every common vertex of the two paths.

   lemma tree_branchpoint (hT : T.IsAcyclic) {x y z : V}
       (p : T.Walk x y) (q : T.Walk x z) (r : T.Walk y z)
       (hp : p.IsPath) (hq : q.IsPath) (hr : r.IsPath) :
       ∃ b, ∃ hbp : b∈p.support,
         b∈q.support ∧ b∈r.support ∧
           ∀ w∈p.support,w∈q.support → w∈(p.takeUntil b hbp).support := by
   …