English
If a graph G is strongly regular with parameters (n, k, ℓ, μ) and n > 0, then k(k − ℓ − 1) = (n − k − 1)μ.
Русский
Если граф G является сильно регулярным с параметрами (n, k, ℓ, μ) и n > 0, то выполняется равенство k(k − ℓ − 1) = (n − k − 1)μ.
LaTeX
$$$k\,(k-\ell-1) = (n-k-1)\,\mu.$$$
Lean4
/-- The parameters of a strongly regular graph with at least one vertex satisfy
`k * (k - ℓ - 1) = (n - k - 1) * μ`. -/
theorem param_eq {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : G.IsSRGWith n k ℓ μ)
(hn : 0 < n) : k * (k - ℓ - 1) = (n - k - 1) * μ :=
by
letI := Classical.decEq V
rw [← h.card, Fintype.card_pos_iff] at hn
obtain ⟨v⟩ := hn
convert card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
· simp [h.regular v]
· simp [h.compl.regular v]
· intro w hw
rw [mem_neighborFinset] at hw
simp_rw [bipartiteAbove, ← mem_neighborFinset, filter_mem_eq_inter]
have s : { v } ⊆ G.neighborFinset w \ G.neighborFinset v :=
by
rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
exact ⟨hw.symm, G.notMem_neighborFinset_self v⟩
rw [inter_comm, neighborFinset_compl, ← inter_sdiff_assoc, ← sdiff_eq_inter_compl, card_sdiff_of_subset s,
card_singleton, ← sdiff_inter_self_left, card_sdiff_of_subset inter_subset_left]
congr
· simp [h.regular w]
· simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw, ← Set.toFinset_card]
congr!
· intro w hw
simp_rw [neighborFinset_compl, mem_sdiff, mem_compl, mem_singleton, mem_neighborFinset, ← Ne.eq_def] at hw
simp_rw [bipartiteBelow, adj_comm, ← mem_neighborFinset, filter_mem_eq_inter, neighborFinset_def, ←
Set.toFinset_inter, ← h.of_not_adj hw.2.symm hw.1, ← Set.toFinset_card]
congr!
