Theorems · Inductive type · combinatorics

SimpleGraph.CompleteEquipartiteSubgraph

{V : Type u_1} → SimpleGraph V → ℕ → ℕ → Type u_1

A complete equipartite subgraph in r > 0 parts each of size t ≠ 0 in G is r subsets of vertices each of size t such that vertices in distinct subsets are adjacent. If r > 0 but t = 0, then parts = {{}}. If r = 0, then parts = {}. These are the two distinct "empty" complete equipartite subgraphs, that is, the complete equipartite subgraphs having no vertices.

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

14 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms