chromaticNumber — Mathlib

English

The chromatic number of the complete multipartite graph on V is the number of parts, i.e., card ι.

Русский

Хроматическое число полного мультитипного графа равно количеству частей, то есть card(ι).

LaTeX

$$$\chi(\text{completeMultipartiteGraph } V) = |\iota|$$$

Lean4

theorem chromaticNumber [Fintype ι] (f : ∀ (i : ι), V i) :
    (completeMultipartiteGraph V).chromaticNumber = Fintype.card ι :=
  by
  apply le_antisymm (colorable V).chromaticNumber_le
  by_contra! h
  exact not_cliqueFree_of_le_card V f le_rfl <| cliqueFree_of_chromaticNumber_lt h

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