OAI/Topology/ArtinGroups/ParabolicIntersections/OrbitEdgeGraph.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The connected subtree generated by an orbit of one edge.

  1. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbitEdgeGraph line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_base_adj line 21
  3. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_translate line 25
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_reachable_generator line 37
  5. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbitVertices line 64
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_reachable line 67
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_adj_mem line 75
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_walk_support line 82
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_graph_le line 96
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.orbit_smul_mem line 103