English
Complete graphs are strongly regular; the parameters are determined by the order n and μ equals any value for μ.
Русский
Полные графы являются сильнострогог-регулярными; параметры зависятся от числа вершин n, а μ может принимать любое значение.
LaTeX
$$top : (⊤ : SimpleGraph V).IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ$$
Lean4
/-- Complete graphs are strongly regular. Note that `μ` can take any value
for complete graphs, since there are no distinct pairs of non-adjacent vertices. -/
theorem top : (⊤ : SimpleGraph V).IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ
where
card := rfl
regular := IsRegularOfDegree.top
of_adj _ _ := card_commonNeighbors_top
of_not_adj v w h h' := (h' ((top_adj v w).2 h)).elim
