Theorems · Definition · combinatorics

SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraph

{r t : ℕ} →
  SimpleGraph.completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph (Function.const (Fin r) (Fin t))

A completeEquipartiteGraph is isomorphic to a corresponding completeMultipartiteGraph. The difference is that the former vertices are a product type whereas the latter vertices are a dependent product type.

Defined in

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Cited by

1 results in Mathlib

Foundations

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