Reachability classes coincide or are disjoint

Proved

WilliamsonShmoys.connected_component_partition_reachable_classes_partition__p2m_aaa6544b_d68f_4c85_b504_f8764908a143_a3

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

approximation-algorithmsplanar-graphstreewidth

Any two reachability classes are equal or disjoint. This supplies pairwise disjointness of distinct parts in the parent. For the equal case, split on whether the classes intersect: a common reachable vertex and symmetry and transitivity of reachability show the representatives are mutually reachable, which makes the classes equal. If there is no common member, the finsets are disjoint by definition. The statement has no restrictions beyond the given vertices, so it also covers isolated vertices.

Preamble

import Mathlib
open Classical
open SimpleGraph

Formal statement

theorem WilliamsonShmoys.connected_component_partition_reachable_classes_partition__p2m_aaa6544b_d68f_4c85_b504_f8764908a143_a3 {V : Type} [Fintype V] [LinearOrder V] (M : SimpleGraph V) (u v : V) : Finset.univ.filter (fun w => M.Reachable u w) = Finset.univ.filter (fun w => M.Reachable v w) ∨ Disjoint (Finset.univ.filter (fun w => M.Reachable u w)) (Finset.univ.filter (fun w => M.Reachable v w)) := 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