OAI/Topology/ArtinGroups/ParabolicIntersections/TreeSeparatedPaths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Distances between different branches of a tree.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.reverse_append_of_common line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.dist_sum_of_branches line 24