Root deletion and connected remainder unions

Every component left after deleting a root from a connected set contains a neighbor of that root. Distinct components give distinct neighbors, so their number is bounded by the root's degree. Small connected sets rooted at those neighbors join to a connected set after the root is restored.

theorem Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Internal.exists_root_neighbor {V : Type} (B : SimpleGraph V) {S : Finset V} {root : V} (member : root ∈ S) (connected : (SimpleGraph.induce {v : V | v ∈ S} B).Connected) (C : (SimpleGraph.induce {v : V | v ∈ S.erase root} B).ConnectedComponent) : ∃ v ∈ PathSystem.region B (S.erase root) C, B.Adj root v

theorem Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Internal.card_components_erase_le_degree {V : Type} [Fintype V] (B : SimpleGraph V) {S : Finset V} {root : V} (member : root ∈ S) (connected : (SimpleGraph.induce {v : V | v ∈ S} B).Connected) : Nat.card (SimpleGraph.induce {v : V | v ∈ S.erase root} B).ConnectedComponent ≤ B.degree root

theorem Algebraic.Cutwidth.Bisection.RedBlack.ConnectedPartition.Internal.connected_insert_biUnion {V : Type} (B : SimpleGraph V) {ι : Type} (root : V) (A : ι → Finset V) (neighbor : ι → V) (adjacent : ∀ (i : ι), B.Adj root (neighbor i)) (rooted : ∀ (i : ι), A i = ∅ ∨ neighbor i ∈ A i ∧ (SimpleGraph.induce {v : V | v ∈ A i} B).Connected) (indices : Finset ι) : (SimpleGraph.induce {v : V | v ∈ insert root (indices.biUnion A)} B).Connected