isBipartiteWith_sum_degrees_eq_twice_card_edges

English

For a locally finite graph G that is bipartite with s,t, the sum of the degrees over s ∪ t equals twice the number of edges.

Русский

Для локально конечного графа G, который двудольный с частями s и t, сумма степеней вершин в s ∪ t равна удвоенному числу ребер.

LaTeX

$$$[G.LocallyFinite] (h : G.IsBipartiteWith s t) ⇒ \sum_{v \in s \cup t} G.degree(v) = 2 \cdot \#G.edgeFinset$$$

Lean4

theorem isBipartiteWith_sum_degrees_eq_twice_card_edges [DecidableEq V] (h : G.IsBipartiteWith s t) :
    ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset :=
  by
  have hsub : G.support ⊆ ↑s ∪ ↑t := isBipartiteWith_support_subset h
  rw [← coe_union, ← Set.toFinset_subset] at hsub
  rw [← Finset.sum_subset hsub, ← sum_degrees_support_eq_twice_card_edges]
  intro v _ hv
  rwa [Set.mem_toFinset, ← degree_eq_zero_iff_notMem_support] at hv

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