English
The sum of degrees over the vertices that lie in the support of the graph equals twice the number of edges.
Русский
Сумма степеней вершин, входящих в опору графа, равна удвоенному числу рёбер.
LaTeX
$$$\sum_{v \in G.support} G.degree(v) = 2 \cdot \#G.edgeFinset$$$
Lean4
/-- The degree-sum formula only counting over the vertices that form edges.
See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version. -/
theorem sum_degrees_support_eq_twice_card_edges : ∑ v ∈ G.support, G.degree v = 2 * #G.edgeFinset := by
classical
simp_rw [← sum_degrees_eq_twice_card_edges, ← sum_add_sum_compl G.support.toFinset, left_eq_add]
apply Finset.sum_eq_zero
intro v hv
rw [degree_eq_zero_iff_notMem_support]
rwa [mem_compl, Set.mem_toFinset] at hv