Edge inclusion controls graph edge counts

Proved

SimpleGraphEdgeCardMonotone__p2m_cf08a975_8aa0_46e9_901e_a88c02c5eb25_a3

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

approximation-algorithmsplanar-graphstreewidth

For finite simple graphs on a finite linearly ordered vertex type, adjacency inclusion gives edgeFinset inclusion and hence nondecreasing cardinality. If reverse adjacency inclusion fails, an edge belongs to K's edgeFinset but not G's, so the inclusion is strict and the cardinality inequality is strict.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem SimpleGraphEdgeCardMonotone__p2m_cf08a975_8aa0_46e9_901e_a88c02c5eb25_a3
    {V : Type} [Fintype V] [LinearOrder V]
    (G K : SimpleGraph V)
    (h : ∀ u v, G.Adj u v → K.Adj u v) :
    (letI : DecidableRel G.Adj := Classical.decRel G.Adj
     letI : DecidableRel K.Adj := Classical.decRel K.Adj
     G.edgeFinset.card ≤ K.edgeFinset.card) ∧
    (letI : DecidableRel G.Adj := Classical.decRel G.Adj
     letI : DecidableRel K.Adj := Classical.decRel K.Adj
     (¬ (∀ u v, K.Adj u v → G.Adj u v) →
       G.edgeFinset.card < K.edgeFinset.card)) := 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