OAI/Topology/ArtinGroups/ParabolicIntersections/TreeShortcutPosition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Interior segments and prefixes in the shortcut metric.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.tree_walk_level line 13
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.exists_interior_segment line 25

    Source documentation

    A long shortcut path contains a translate of the fixed segment well inside both ends, and at bounded distance from its first end.

    theorem exists_interior_segment (hT : T.IsTree) (hA : PreservesAdj (G := G) T)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj

  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.bounded_vertices_in_prefix line 78