OAI/Topology/ArtinGroups/ParabolicIntersections/TreeActionDefinitions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Basic data for actions on simplicial trees.

  1. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj line 11
  2. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.translate line 13
  3. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer line 16
  4. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PathClosed line 20

    Source documentation

    A set contains the unique path between any two of its vertices.

    def PathClosed (T : SimpleGraph V) (U : Set V) : Prop :=
…