OAI/Topology/ArtinGroups/ParabolicIntersections/VisualTreeProperties.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_preservesAdj line 16
2. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_vertex_proper line 21
3. lemma OAI.HarmonicArtin.ParabolicIntersections.visual_branching line 34

   Source documentation

   Every direction at every vertex can be moved by its stabilizer.

   lemma visual_branching (v w : VisualVertex M Y Z) (h : (visualGraph M Y Z).Adj v w) :
       ∃ a : Artin M, a • v=v ∧ a • w≠w := by
   …

   Mentions: OAI.HarmonicArtin.ParabolicIntersections.VisualVertex, OAI.HarmonicArtin.ParabolicIntersections.visualGraph, OAI.HarmonicArtin.Artin