completeEquipartiteGraph_colorable

English

For every r and t, the complete equipartite graph with parts of sizes r and t is r-colorable; there exists a proper coloring with r colors.

Русский

Для любых r и t полный экпартитный граф с частями размеров r и t допускает раскраску в r цветов; существует допустимая раскраска в r цветов.

LaTeX

$$$\exists c: (\text{completeEquipartiteGraph } r\ t).V \to \mathrm{Fin}(r),\; \forall x,y,\ (\text{completeEquipartiteGraph } r\ t).Adj\ x\ y \to c(x) \neq c(y).$$$

Lean4

/-- The `completeEquipartiteGraph r t` is always `r`-colorable. -/
theorem completeEquipartiteGraph_colorable : (completeEquipartiteGraph r t).Colorable r :=
  ⟨Coloring.completeEquipartiteGraph⟩

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