English
Let G be locally finite and bipartite with s,t. Then the sum of degrees of vertices in s equals the sum of degrees of vertices in t.
Русский
Пусть G локально конечно; если G двудольный с частями s и t, то сумма степеней вершин в s равна сумме степеней вершин в t.
LaTeX
$$[G.LocallyFinite] (h : G.IsBipartiteWith s t) ⇒ ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w$$
Lean4
/-- If `G.IsBipartiteWith s t`, then the sum of the degrees of vertices in `s` is equal to the sum
of the degrees of vertices in `t`.
See `Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`. -/
theorem isBipartiteWith_sum_degrees_eq [G.LocallyFinite] (h : G.IsBipartiteWith s t) :
∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w :=
by
simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]
conv_lhs =>
rhs; intro v
rw [isBipartiteWith_bipartiteAbove h v.prop]
conv_rhs =>
rhs; intro w
rw [isBipartiteWith_bipartiteBelow h w.prop]
simp_rw [sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w), sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]
exact sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj
