Subcubic Brooks theorem: ComponentAttachments

Part of the proof that a finite subcubic K₄-free graph is three-colourable.

theorem BrooksSubcubic.mem_of_walk_closed {V : Type u_1} (G : SimpleGraph V) (W : Set V) (hW : ∀ w ∈ W, ∀ (y : V), G.Adj w y → y ∈ W) {u v : V} (p : G.Walk u v) : u ∈ W → v ∈ W

If W is closed under G-adjacency, a walk starting in W stays in W.

theorem BrooksSubcubic.exists_adj_in_class {V : Type u_1} (G : SimpleGraph V) (hconn : G.Connected) {x d : V} (hd : d ≠ x) : ∃ (z : V), G.Adj x z ∧ ∃ (hz : z ≠ x), (SimpleGraph.induce {x}ᶜ G).connectedComponentMk ⟨d, hd⟩ = (SimpleGraph.induce {x}ᶜ G).connectedComponentMk ⟨z, hz⟩

Linchpin. In a connected G, for any d ≠ x, x is adjacent to some vertex z in the same G−x-component as d.