Summing edge bounds over connected components

Proved

SimpleGraphComponentEdgeSumBound

by xuanji · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theoryplanar-graphs

Let $G$ be a finite simple graph. Assume that every connected component $c$ satisfies the induced-component edge bound

|E(G[c])|\le 3|V(c)|.

Then the whole graph satisfies

|E(G)|\le 3|V(G)|.

The theorem packages the finite disjoint decomposition of the vertex and edge sets into connected components.

Preamble

import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
import Definitions.Def_OrdinaryPolygonalDrawing

open Classical
noncomputable section

Formal statement

lemma SimpleGraphComponentEdgeSumBound {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype G.edgeSet]
    (hcomp : ∀ c : G.ConnectedComponent,
      (G.induce c.supp).edgeFinset.card ≤ 3 * Fintype.card c.supp) :
    G.edgeFinset.card ≤ 3 * Fintype.card V := by sorry

Source

https://github.com/wpegden/crossing-consequences/blob/8769d142033fce042f502bf2857afb6b1375b5c3/Tablet/SimpleGraphComponentEdgeSumBound.lean#L1-L101

View graph