compl — Mathlib

English

The complement of a strongly regular graph is again strongly regular with parameters n, n − k − 1, n − (2k − μ) − 2, n − (2k − ℓ).

Русский

Комплемент сильно регулярного графа снова сильно регулярен с параметрами n, n − k − 1, n − (2k − μ) − 2, n − (2k − ℓ).

LaTeX

$$$G^{\mathsf{c}}.IsSRGWith(n,\, n-k-1,\, n-(2k-μ)-2,\, n-(2k-ℓ))$$$

Lean4

/-- The complement of a strongly regular graph is strongly regular. -/
theorem compl (h : G.IsSRGWith n k ℓ μ) : Gᶜ.IsSRGWith n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ))
    where
  card := h.card
  regular := h.compl_is_regular
  of_adj _ _ := h.card_commonNeighbors_eq_of_adj_compl
  of_not_adj _ _ := h.card_commonNeighbors_eq_of_not_adj_compl

Похожие утверждения