Components of graphs of maximum degree two #
A connected component of a graph with maximum degree at most 2 (a path or a cycle) contains
at most two vertices of degree at most 1. This is the combinatorial input to the Kempe chain
step of Vizing's theorem.
theorem
LeanPool.Vizing.degree_toSimpleGraph_le
{V : Type u_1}
[Fintype V]
{H : SimpleGraph V}
[DecidableRel H.Adj]
(Cp : H.ConnectedComponent)
[(z : ↥Cp) → Fintype ↑(Cp.toSimpleGraph.neighborSet z)]
(z : ↥Cp)
:
Degrees can only drop when passing to the induced graph on a connected component.
theorem
LeanPool.Vizing.no_three_endpoints
{V : Type u_1}
[Fintype V]
{H : SimpleGraph V}
[DecidableRel H.Adj]
(hdeg : ∀ (z : V), H.degree z ≤ 2)
{u v w : V}
(huv : u ≠ v)
(huw : u ≠ w)
(hvw : v ≠ w)
(hu : H.degree u ≤ 1)
(hv : H.degree v ≤ 1)
(hw : H.degree w ≤ 1)
(h1 : H.Reachable u v)
(h2 : H.Reachable u w)
:
In a graph of maximum degree at most 2, no connected component contains three distinct
vertices of degree at most 1.