English
There is an isomorphism between the complete equipartite graph in r parts of size t and the Turán graph with (rt) vertices and r parts.
Русский
Существует изоморфизм между полным равновешенным графом с r частями по t вершин в каждой и графом Турэна с rt вершинами и r частями.
LaTeX
$$completeEquipartiteGraph r t ≃g turanGraph (r \cdot t) r$$
Lean4
/-- The **complete equipartite graph** in `r` parts each of *equal* size `t` such that two
vertices are adjacent if and only if they are in different parts, often denoted $K_r(t)$.
This is isomorphic to a corresponding `completeMultipartiteGraph` and `turanGraph`. The difference
is that the former vertices are a product type.
See `completeEquipartiteGraph.completeMultipartiteGraph`, `completeEquipartiteGraph.turanGraph`. -/
abbrev completeEquipartiteGraph (r t : ℕ) : SimpleGraph (Fin r × Fin t) :=
SimpleGraph.comap Prod.fst ⊤
