Theorems · Definition · combinatorics

SimpleGraph.completeEquipartiteGraph

(r t : ℕ) → SimpleGraph (Fin r × Fin t)

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.

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

12 results in Mathlib

Foundations

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