Incidence counts in finite simple graphs

theorem ACMax.cross_count {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (X Y : Finset V) : ∑ v ∈ X, (G.neighborFinset v ∩ Y).card = ∑ w ∈ Y, (G.neighborFinset w ∩ X).card

Bipartite double count (generic-V port of cross_count_nineteen): for any two vertex sets, the X→Y incidences equal the Y→X incidences. The DecidableEq binder lets the lemma instantiate to whichever instance the call site elaborated with (instDecidableEqFin at Fin n, Classical.propDecidable at generic V).

theorem ACMax.sum_adj_eq_single {V : Type u_1} {R : Type u_2} [AddCommMonoid R] (G : SimpleGraph V) (A B : Finset V) (a b : V) (weight : V → V → R) (ha : a ∈ A) (hb : b ∈ B) (hsupport : ∀ i ∈ A, ∀ j ∈ B, G.Adj i j → i = a ∧ j = b) : (∑ i ∈ A, ∑ j ∈ B, if G.Adj i j then weight i j else 0) = if G.Adj a b then weight a b else 0

A weighted adjacency sum supported on one pair is its contribution at that pair.