Maximal extension for a hereditary property on a finite graph type
Provedfinite_hereditary_maximal_extension__p2m_3f244f53_8936_4715_8547_0063dd70ff12_a1approximation-algorithmsplanar-graphstreewidth
If a property of simple graphs on a finite vertex type is inherited by subgraphs, every graph satisfying it has a supergraph satisfying it that is maximal among such supergraphs.
Preamble
import Mathlib
Formal statement
theorem finite_hereditary_maximal_extension__p2m_3f244f53_8936_4715_8547_0063dd70ff12_a1
{V : Type} [Fintype V]
(K : SimpleGraph V)
(P : SimpleGraph V → Prop)
(hK : P K)
(hdown : ∀ {G H : SimpleGraph V}, G ≤ H → P H → P G) :
∃ H : SimpleGraph V,
K ≤ H ∧ P H ∧
∀ J : SimpleGraph V, K ≤ J → P J → H ≤ J → J = H := 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).