English
Let G be a finite strongly regular graph with parameters (n, k, ℓ, μ). For any distinct vertices v and w that are adjacent in G, the number of common neighbors of v and w in the complement Gᶜ is exactly n − (2k − ℓ).
Русский
Пусть G — конечный строго регулярный граф с параметрами (n, k, ℓ, μ). Для любых различных вершин v и w, которые смежны в G, число общих соседей v и w в комплементе Gᶜ равно n − (2k − ℓ).
LaTeX
$$$\text{If } G \text{ is SRG with parameters } (n,k,\ell,\mu)\text{ and } v \neq w\text{ with } G(v,w),\text{ then } |G^{\mathsf{c}}\text{ commonNeighbors }(v,w)| = n - (2k - \ell).$$$
Lean4
theorem card_commonNeighbors_eq_of_not_adj_compl (h : G.IsSRGWith n k ℓ μ) {v w : V} (hn : v ≠ w) (hna : ¬Gᶜ.Adj v w) :
Fintype.card (Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ) :=
by
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl, Set.toFinset_diff,
Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
simp only [not_and, Classical.not_not, compl_adj] at hna
have h2' := hna hn
simp_rw [compl_neighborFinset_sdiff_inter_eq, sdiff_compl_neighborFinset_inter_eq h2']
rwa [← Finset.compl_union, card_compl, h.card_neighborFinset_union_of_adj, ← h.card]
