completeEquipartiteGraph — Mathlib

English

Let r and t be natural numbers. The complete equipartite graph with parts of sizes r and t admits an r-coloring, given by coloring each vertex by the first coordinate.

Русский

Пусть r и t — натуральные числа. Полный равнопартитный граф с частями размеров r и t имеет раскраску в 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 injection `(x₁, x₂) ↦ x₁` is always a `r`-coloring of a `completeEquipartiteGraph r ·`. -/
def completeEquipartiteGraph : (completeEquipartiteGraph r t).Coloring (Fin r) :=
  ⟨Prod.fst, id⟩

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