OAI/Topology/ArtinGroups/ParabolicIntersections/TreePeriodicPaths.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Iterating a tree segment without backtracking produces an actual translation axis.

  1. abbrev OAI.HarmonicArtin.ParabolicIntersections.TreeAction.shiftHom line 13
  2. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath line 15
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_length line 21
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.first_append_nonempty line 32
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_reverse_snd line 38
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.nil_copy_append line 55
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_isPath line 60
  8. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodic_orbit_distance line 88
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_support_step line 95
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_translate_mem line 100
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_translate_mem_of_lt line 108
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_vertex_mem line 120
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.periodicPath_snd line 127