Partitioning the large black components

Lift connected partitions of individual black components to the original vertex type and combine them. Distinct components have disjoint supports, so the resulting pieces partition the complement of the small components. Summing the componentwise bounds controls the total number of pieces.

theorem Algebraic.Cutwidth.Bisection.RedBlack.Internal.exists_large_component_partition {V : Type} [Fintype V] (B : SimpleGraph V) (degree : ∀ (v : V), B.degree v ≤ 3) (M : ℕ) (positive : 0 < M) (U : Finset V) (small_iff : ∀ (v : V), v ∈ U ↔ Fintype.card ↥(B.connectedComponentMk v) ≤ M) : ∃ (parts : Finset (Finset V)), parts.biUnion id = Finset.univ \ U ∧ (↑parts).Pairwise Disjoint ∧ (∀ P ∈ parts, (SimpleGraph.induce {v : V | v ∈ P} B).Connected ∧ P.card ≤ 3 * M) ∧ M * parts.card ≤ 2 * (Finset.univ \ U).card