colorable_of_cliqueFree — Mathlib

English

If the complete multipartite graph is clique-free at n, then it is colorable with n−1 colors.

Русский

Если граф, являющийся полным мультитипным, не содержит клики размера n, то он очередной раскраской может быть окрашен в n−1 цветов.

LaTeX

$$$\text{CliqueFree}_{{(completeMultipartiteGraph V)}}(n) \Rightarrow \text{Colorable}(n-1)$$$

Lean4

theorem colorable_of_cliqueFree (f : ∀ (i : ι), V i) (hc : (completeMultipartiteGraph V).CliqueFree n) :
    (completeMultipartiteGraph V).Colorable (n - 1) := by
  cases n with
  | zero => exact absurd hc not_cliqueFree_zero
  | succ n =>
    have : Fintype ι := fintypeOfNotInfinite fun hinf ↦ not_cliqueFree_of_infinite V f hc
    apply (coloring V).colorable.mono
    have := not_cliqueFree_of_le_card V f le_rfl
    contrapose! this
    exact hc.mono this

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