Handshake_Lemma
Provedcombinatoricsgraph-theoryproofwiki
In any finite simple graph, the sum of all vertex degrees equals twice the number of edges.
Preamble
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
Formal statement
theorem Handshake_Lemma {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