Theorems · Theorem · combinatorics

SimpleGraph.IsSRGWith.compl

∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V], G.IsSRGWith n k ℓ μ → Gᶜ.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))

The complement of a strongly regular graph is strongly regular.

Defined in

Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Cited by

1 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRelDecidableEq