cliqueFree_of_chromaticNumber_lt — Mathlib

English

If the chromatic number χ(G) < n, then G has no K_n.

Русский

Если χ(G) < n, то K_n не содержится в G.

LaTeX

$$$\chi(G) < n \implies G\text{ is }K_n\text{-free}$$$

Lean4

theorem cliqueFree_of_chromaticNumber_lt {n : ℕ} (hc : G.chromaticNumber < n) : G.CliqueFree n :=
  by
  have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top
  obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne
  have := colorable_chromaticNumber hc'
  refine this.cliqueFree ?_
  rw [← ENat.coe_toNat_eq_self] at hne
  rw [← hne] at hc
  simpa using hc

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