chromaticNumber — Mathlib

English

If both parts are nonempty, the chromatic number of the complete bipartite graph K_{V,W} is 2.

Русский

Если обе части непусты, хроматическое число полного двудольного графа равно 2.

LaTeX

$$$\chi(K_{V,W}) = 2$$$

Lean4

theorem chromaticNumber {V W : Type*} [Nonempty V] [Nonempty W] : (completeBipartiteGraph V W).chromaticNumber = 2 :=
  by
  rw [← Nat.cast_two,
    chromaticNumber_eq_iff_forall_surjective (by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable)]
  intro C b
  have v := Classical.arbitrary V
  have w := Classical.arbitrary W
  have h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w) := by simp
  by_cases he : C (Sum.inl v) = b
  · exact ⟨_, he⟩
  by_cases he' : C (Sum.inr w) = b
  · exact ⟨_, he'⟩
  · simpa using two_lt_card_iff.2 ⟨_, _, _, C.valid h, he, he'⟩

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