turanGraph — Mathlib

English

The canonical (r+1)-clique-free Turán graph on n vertices is the graph on Fin n in which two vertices are adjacent precisely when their residues modulo r are different.

Русский

Канонический граф Турэна на n вершинах, не содержащий клики размера r+1, строится на вершинах Fin n так, что две вершины соседствуют тогда, когда их остатки по модулю r различны.

LaTeX

$$$\mathrm{turanGraph}(n,r) : \text{SimpleGraph}(\mathrm{Fin}\,n) \\text{Adj}(v,w) \iff v \bmod r \neq w \bmod r.$$$

Lean4

/-- The canonical `r + 1`-cliquefree Turán graph on `n` vertices. -/
def turanGraph (n r : ℕ) : SimpleGraph (Fin n) where Adj v w := v % r ≠ w % r

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