OAI/Topology/ArtinGroups/ParabolicIntersections/TreePathMetric.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Distance and path-support facts used by the tree acylindrification.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_length_eq_dist line 9
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_metric_additive line 17
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_support_subset_walk line 24
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_support_subset_append line 32