The internal-degree sum of a vertex set is even

For any finite simple graph G and vertex set s, the sum over v ∈ s of the number of neighbours of v lying in s equals twice the number of edges internal to s, hence is even.

theorem ACMax.sum_inDegree_even {V : Type u_1} [Fintype V] (G : SimpleGraph V) (s : Finset V) : Even (∑ v ∈ s, (G.neighborFinset v ∩ s).card)

∑_{v ∈ s} |N(v) ∩ s| is even (it counts each internal edge twice).