OAI/Geometry/HyperbolicGroups/PictureOutsideColor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexRepresentative line 20
2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexClass_representative line 22
3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexColor line 25
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.color_eq_on_vertex_outside line 32

   Source documentation

   Outside a set containing every edge-color boundary, incident face colors agree around the ENTIRE literal vertex rotation orbit.

   lemma color_eq_on_vertex_outside {C : Type*} (color : D → C)
       (hface : ∀ x, color (M.face x) = color x) (S : Set M.GraphVertex)
       (hboundary : ∀ x, color (M.edge x) ≠ color x → M.vertexClass x ∈ S)
       (x y : D) (hv : M.vertexClass x = M.vertexClass y) (hx : M.vertexClass x ∉ S) :
       color x = color y := by
   …

5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexColor_eq_dart_outside line 56
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexColor_adj_outside line 65
7. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexColor_connected_outside line 79

   Source documentation

   A connected set of primal vertices off the rooted separator carries one deleted-dual-component color. This closes the actual separation bridge from rotation-system boundaries to the underlying graph.

   theorem vertexColor_connected_outside {C : Type*} (color : D → C)
       (hface : ∀ x, color (M.face x) = color x) (S : Set M.GraphVertex)
       (hboundary : ∀ x, color (M.edge x) ≠ color x → M.vertexClass x ∈ S)
       (U : Set M.GraphVertex) (hU : ∀ v ∈ U, v ∉ S)
       (hconn : (M.underlyingGraph.induce U).Preconnected) :
       ∀ v ∈ U, ∀ w ∈ U, M.vertexColor color v = M.vertexColor color w := by
   …