chromaticNumber_top — Mathlib

English

For a finite vertex set V, the chromatic number of the complete graph on V equals the cardinality of V.

Русский

Для конечного множества вершин V хроматическое число полного графа на V равно мощности V (кардинале).

LaTeX

$$$\chi(\top_V) = |V|$$$

Lean4

@[simp]
theorem chromaticNumber_top [Fintype V] : (⊤ : SimpleGraph V).chromaticNumber = Fintype.card V :=
  by
  rw [chromaticNumber_eq_card_iff_forall_surjective (selfColoring _).colorable]
  intro C
  rw [← Finite.injective_iff_surjective]
  intro v w
  contrapose
  intro h
  exact C.valid h

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