sum_degrees_support_eq_twice_card_edges

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

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