completeMultipartiteGraph — Mathlib

English

The complete equipartite graph K_r(t) is isomorphic to a corresponding complete multipartite graph with a dependent product index.

Русский

Полный равновесный граф K_r(t) изоморфен соответствующему полному мультитипному графу с зависимым произведением индексов.

LaTeX

$$completeEquipartiteGraph r t ≃g completeMultipartiteGraph (Function.const (Fin r) (Fin t))$$

Lean4

/-- 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. -/
def completeMultipartiteGraph :
    completeEquipartiteGraph r t ≃g completeMultipartiteGraph (Function.const (Fin r) (Fin t)) :=
  { (Equiv.sigmaEquivProd (Fin r) (Fin t)).symm with map_rel_iff' := by simp }

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