sum_degrees_eq_twice_card_edges — Mathlib

English

Let G be a finite graph. Then the sum of the degrees of all vertices equals twice the number of edges.

Русский

Пусть G — конечный граф. Тогда сумма степеней вершин равна удвоенному числу рёбер.

LaTeX

$$$\sum_v G.degree(v) = 2 \cdot \#G.edgeFinset$$$

Lean4

/-- The degree-sum formula.  This is also known as the handshaking lemma, which might
more specifically refer to `SimpleGraph.even_card_odd_degree_vertices`. -/
theorem sum_degrees_eq_twice_card_edges : ∑ v, G.degree v = 2 * #G.edgeFinset :=
  G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges

Похожие утверждения