OAI/Topology/ArtinGroups/ParabolicIntersections/TreeBridge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A group preserving both sides of a bridge fixes its endpoints.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.snd_append_of_not_nil line 11
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.fixes_bridge line 19

    Source documentation

    The endpoint-exit condition identifies a bridge between two convex sets. Comparing its length with a translated path forces both endpoints to be fixed.

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

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj