An inclusion-maximal planar graph is connected
OpenWilliamsonShmoys_maximal_planar_graph_connected__p2m_f305e987_8fa4_48f1_bb88_04ada6b91b35_a2approximation-algorithmsplanar-graphstreewidth
A planar graph on at least three vertices that has no strictly larger planar supergraph on the same vertices is connected. If it were disconnected, an arc in the unbounded face could join exposed vertices of distinct components and give a larger planar supergraph.
Preamble
import Definitions.Def_WilliamsonShmoys_PlanarDrawingOn import Mathlib set_option autoImplicit false
Formal statement
theorem WilliamsonShmoys_maximal_planar_graph_connected__p2m_f305e987_8fa4_48f1_bb88_04ada6b91b35_a2
{V : Type} [Fintype V] [LinearOrder V]
(G : SimpleGraph V) (hcard : 3 ≤ Fintype.card V)
(hG : WilliamsonShmoys.HasPlanarDrawingOn G)
(hmax : ∀ K : SimpleGraph V, G ≤ K → WilliamsonShmoys.HasPlanarDrawingOn K → K = G) :
G.Connected := by
sorrySource
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).