bicoloring — Mathlib

English

The complete bipartite graph K_{V,W} admits a proper 2-coloring by partitioning vertices into the left and right parts.

Русский

Полный двудольный граф K_{V,W} допускает корректное 2-окрашивание за счет деления вершин на левую и правую части.

LaTeX

$$$\exists c: (completeBipartiteGraph V W).Coloring\{0,1\}, \; \forall x,y,\; \mathrm{Adj}(x,y) \Rightarrow c(x) \neq c(y)$$$

Lean4

/-- The bicoloring of a complete bipartite graph using whether a vertex
is on the left or on the right. -/
def bicoloring (V W : Type*) : (completeBipartiteGraph V W).Coloring Bool :=
  Coloring.mk (fun v => v.isRight)
    (by
      intro v w
      cases v <;> cases w <;> simp)

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