Handshake_Lemma_v2
Provedgraph-theoryhandshake-lemmanamed-theoremsproofwikivertices-of-graphs
In an undirected graph, the sum of the degrees of all vertices equals twice the number of edges.
Preamble
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
Formal statement
theorem Handshake_Lemma_v2 {V : Type _} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (Finset.univ.sum fun v => G.degree v) = 2 * G.edgeFinset.card := by sorrySource