Subcubic Brooks theorem: CutPartition #
Part of the proof that a finite subcubic K₄-free graph is three-colourable.
theorem
BrooksSubcubic.connected_induce_insert_of_component_neighbors
{V : Type u_1}
[DecidableEq V]
(G : SimpleGraph V)
(x : V)
(A : Finset V)
(P : (SimpleGraph.induce {x}ᶜ G).ConnectedComponent → Prop)
(hmem : ∀ (v : V), v ∈ A ↔ ∃ (hv : v ≠ x), P ((SimpleGraph.induce {x}ᶜ G).connectedComponentMk ⟨v, hv⟩))
(hneigh :
∀ (C : (SimpleGraph.induce {x}ᶜ G).ConnectedComponent),
P C → ∃ (z : V), G.Adj x z ∧ ∃ (hz : z ≠ x), (SimpleGraph.induce {x}ᶜ G).connectedComponentMk ⟨z, hz⟩ = C)
:
(SimpleGraph.induce (↑(insert x A)) G).Connected
A union of components of the vertex-deleted graph, each attached to the deleted vertex, becomes connected when that vertex is inserted.
theorem
BrooksSubcubic.cut_partition_of_unreachable
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
(hconn : G.Connected)
(x d e : V)
(hd : d ≠ x)
(he : e ≠ x)
(hsep : ¬(SimpleGraph.induce {x}ᶜ G).Reachable ⟨d, hd⟩ ⟨e, he⟩)
: