OAI/Topology/ArtinGroups/ParabolicIntersections/TreeTranslationSegment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Reflecting a segment at both ends constructs a tree translation.

  1. abbrev OAI.HarmonicArtin.ParabolicIntersections.TreeAction.actPath line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.actPath_copy_length line 14
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.actPath_copy_snd line 19
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.actPath_copy_reverse_snd line 26
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.append_first line 34
  6. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.translation_segment line 41