cliqueFree — Mathlib

English

If the chromatic number χ(G) is less than n, then G has no K_n.

Русский

Если хроматическое число графа меньше n, то граф не содержит клики размера n.

LaTeX

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

Lean4

protected theorem cliqueFree {n m : ℕ} (hc : G.Colorable n) (hm : n < m) : G.CliqueFree m :=
  by
  by_contra h
  simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h
  obtain ⟨s, h, rfl⟩ := h
  exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

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