English
For a strongly regular graph, the union of neighbor sets of two vertices has cardinality equal to 2k minus the common neighbors, with a special adjustment when the vertices are adjacent.
Русский
Для строго регулярного графа объединение множеств соседей двух вершин имеет кардинал равный 2k минус общие соседи; при соседстве корректируется.
LaTeX
$$card_neighborFinset_union_eq {v w} (h : G.IsSRGWith n k ℓ μ) → #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card (G.commonNeighbors v w)$$
Lean4
theorem card_neighborFinset_union_eq {v w : V} (h : G.IsSRGWith n k ℓ μ) :
#(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - Fintype.card (G.commonNeighbors v w) :=
by
apply Nat.add_right_cancel (m := Fintype.card (G.commonNeighbors v w))
rw [Nat.sub_add_cancel, ← Set.toFinset_card]
· simp [commonNeighbors, ← neighborFinset_def, Finset.card_union_add_card_inter, h.regular.degree_eq, two_mul]
· apply le_trans (card_commonNeighbors_le_degree_left _ _ _)
simp [h.regular.degree_eq, two_mul]
