V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - ℓ
rw [← h.of_adj v w ha]
no goals
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : IsSRGWith G n k ℓ μ
ha : Adj G v w
⊢ Finset.card (neighborFinset G v ∪ neighborFinset G w) = 2 * k - Fintype.card ↑(commonNeighbors G v w)
apply h.card_neighborFinset_union_eq