The graph on the core pieces

Identify the region vertices of the region-boundary quotient and suppress them. The remaining vertices represent the connected pieces outside all regions; a suppressed region supplies a connection between its neighboring pieces. This is the core graph used by the weighted-tree argument.

noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.PathSuppression.coreGraph {V ι : Type} [Fintype V] [Fintype ι] (B : SimpleGraph V) (P : ι → Finset V) (f : ι ↪ (B.deleteEdges (⋃ (i : ι), ↑(B.cutFinset (P i)))).ConnectedComponent) : SimpleGraph { C : (B.deleteEdges (⋃ (i : ι), ↑(B.cutFinset (P i)))).ConnectedComponent // C ∉ Finset.image (⇑f) Finset.univ }

Suppress the designated region vertices of the boundary quotient.

Equations

• One or more equations did not get rendered due to their size.