card_le_of_coloring — Mathlib

English

For any clique s in G and coloring of the vertex set with α colors, the clique size satisfies |s| ≤ α.

Русский

Для любой клики s в графе G и раскраски вершин α цветами выполняется |s| ≤ α.

LaTeX

$$$|s| \le |\alpha|$$$

Lean4

theorem card_le_of_coloring {s : Finset V} (h : G.IsClique s) [Fintype α] (C : G.Coloring α) :
    s.card ≤ Fintype.card α := by
  rw [isClique_iff_induce_eq] at h
  have f : G.induce ↑s ↪g G := Embedding.comap (Function.Embedding.subtype fun x => x ∈ ↑s) G
  rw [h] at f
  convert Fintype.card_le_of_injective _ (C.comp f.toHom).injective_of_top_hom using 1
  simp

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