Petersen's theorem

TheoremPetersen's theorem on cubic graphs#✓fully proved

Every finite simple graph that is \(3\)-regular and has no bridge, that is, no edge whose removal disconnects its endpoints, has a perfect matching: a set of edges of the graph such that every vertex lies on exactly one of them.

theorem petersen_bridgeless_cubic_has_perfect_matching_general
    {V : Type*} [Fintype V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hreg : G.IsRegularOfDegree 3)
    (hbridge : ∀ e ∈ G.edgeSet, ¬G.IsBridge e) :
    ∃ M : G.Subgraph, M.IsPerfectMatching

Used by 1

Used byPetersen's perfect matching theorem

TheoremPetersen's perfect matching theorem#✓fully proved

Every finite simple graph that is \(3\)-regular and has no bridge, that is, no edge whose removal disconnects its endpoints, has a perfect matching: a set of edges of the graph such that every vertex lies on exactly one of them.

theorem petersen_bridgeless_cubic_has_perfect_matching
    {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hreg : G.IsRegularOfDegree 3)
    (hbridge : ∀ e ∈ G.edgeSet, ¬G.IsBridge e) :
    ∃ M : G.Subgraph, M.IsPerfectMatching

Sources

• J. Petersen, "Die Theorie der regulären graphs", Acta Mathematica 15 (1891), 193-220, DOI 10.1007/BF02392606. It follows from petersen_bridgeless_cubic_has_perfect_matching_general; the instance [DecidableEq V] is unused and keeps the source's shape.

Uses 1

Proof usesPetersen's theorem on cubic graphs

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.