isBipartiteWith_sum_degrees_eq_card_edges'

English

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

Русский

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

LaTeX

$$$\sum_{w \in t} G.degree(w) = \#G.edgeFinset$$$

Lean4

/-- The degree-sum formula for bipartite graphs, summing over the "right" 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 "left". -/
theorem isBipartiteWith_sum_degrees_eq_card_edges' (h : G.IsBipartiteWith s t) : ∑ v ∈ t, G.degree v = #G.edgeFinset :=
  isBipartiteWith_sum_degrees_eq_card_edges h.symm

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