English
If G is SRG, and v,w are not adjacent in the complement, the commonNeighbors cardinality in the complement equals a fixed expression in n,k,ℓ,μ, computed by the formula.
Русский
Если граф слабой регулярности, а вершины не смежны в комплементе, кардинал общих соседей в комплементе определяется выражением из n,k,ℓ,μ.
LaTeX
$$card_commonNeighbors_eq_of_adj_compl (h : G.IsSRGWith n k ℓ μ) {v w : V} (ha : Gᶜ.Adj v w) : Fintype.card (Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2$$
Lean4
theorem card_commonNeighbors_eq_of_adj_compl (h : G.IsSRGWith n k ℓ μ) {v w : V} (ha : Gᶜ.Adj v w) :
Fintype.card (Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2 :=
by
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl, Set.toFinset_diff,
Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]
simp_rw [compl_neighborFinset_sdiff_inter_eq]
have hne : v ≠ w := ne_of_adj _ ha
rw [compl_adj] at ha
rw [card_sdiff_of_subset, ← insert_eq, card_insert_of_notMem, card_singleton, ← Finset.compl_union]
· rw [card_compl, h.card_neighborFinset_union_of_not_adj hne ha.2, ← h.card]
· simp only [hne.symm, not_false_iff, mem_singleton]
· intro u
simp only [mem_union, mem_compl, mem_neighborFinset, mem_inter, mem_singleton]
rintro (rfl | rfl) <;> simpa [adj_comm] using ha.2
