isBipartiteWith_sum_degrees_eq_card_edges

English

If G is bipartite with s,t, then the sum of the degrees over s equals the number of edges.

Русский

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

LaTeX

$$$\sum_{v \in s} G.degree(v) = \#G.edgeFinset$$$

Lean4

/-- The degree-sum formula for bipartite graphs, summing over the "left" part.

See `SimpleGraph.sum_degrees_eq_twice_card_edges` for the general version, and
`SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges'` for the version from the "right". -/
theorem isBipartiteWith_sum_degrees_eq_card_edges (h : G.IsBipartiteWith s t) : ∑ v ∈ s, G.degree v = #G.edgeFinset :=
  by
  classical
  rw [← Nat.mul_left_cancel_iff zero_lt_two, ← isBipartiteWith_sum_degrees_eq_twice_card_edges h,
    sum_union (disjoint_coe.mp h.disjoint), two_mul, add_right_inj]
  exact isBipartiteWith_sum_degrees_eq h

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