Sum component vertex bounds in a disconnected graph

Proved

WilliamsonShmoys.component_bounds_sum_le__p2m_666f06c4_d624_4127_b254_b308e951621e_a1

by Eyal1990 · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximation-algorithmsplanar-graphstreewidth

In a finite disconnected graph, summing three times each component's vertex count minus three is at most three times the total vertex count minus six. This follows from the component supports partitioning the vertices and there being at least two components.

Preamble

import Mathlib

Formal statement

theorem WilliamsonShmoys.component_bounds_sum_le__p2m_666f06c4_d624_4127_b254_b308e951621e_a1
    {V : Type} [Fintype V] [LinearOrder V] (K : SimpleGraph V)
    (hcard : 3 ≤ Fintype.card V) (hdisconn : ¬ K.Connected) :
    letI : Fintype K.ConnectedComponent := Fintype.ofFinite _
    ∑ c : K.ConnectedComponent,
      (letI : Fintype {v : V // v ∈ c.supp} := Fintype.ofFinite _
       3 * Fintype.card {v : V // v ∈ c.supp} - 3) ≤ 3 * Fintype.card V - 6 := by sorry

Source

David P. Williamson and David B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, author electronic manuscript, Section 10.2, proof of Theorem 10.11, pp. 270-272. https://doi.org/10.1017/CBO9780511921735. Bounded tree-width of the pieces: Robertson–Seymour (planar graphs of radius r have tree-width at most 3r+1) / Bodlaender (k-outerplanar graphs have tree-width at most 3k-1).

View graph