turanGraph_adj — Mathlib

English

For the Turán graph on n vertices with parameter r, the adjacency relation is exactly given by non-equality of the residues modulo r.

Русский

Об adjacency в графе Турэна на n вершинах с параметром r задаётся отношением несовпадения остатков по модулю r.

LaTeX

$$$(\mathrm{turanGraph}\, n\, r).\mathrm{Adj}(v,w) \iff v \% r \neq w \% r.$$$

Lean4

theorem turanGraph_adj {v w} : (turanGraph n r).Adj v w ↔ v % r ≠ w % r :=
  .rfl

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