colorable_of_cliqueFree — Mathlib

English

If G is complete multipartite and clique-free of n, then G is colorable with n−1 colors.

Русский

Если G является полным мультитипным и clique-free размера n, то он может быть раскрашен в n−1 цветов.

LaTeX

$$G.IsCompleteMultipartite \Rightarrow G.CliqueFree n \Rightarrow G.Colorable (n-1)$$

Lean4

theorem colorable_of_cliqueFree {n : ℕ} (h : G.IsCompleteMultipartite) (hc : G.CliqueFree n) : G.Colorable (n - 1) :=
  (completeMultipartiteGraph.colorable_of_cliqueFree _ (fun _ ↦ ⟨_, h.setoid.refl _⟩) <|
        hc.comap h.iso.symm.toEmbedding).of_hom
    h.iso

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