surjOn_of_card_le_isClique — Mathlib

English

For a clique s in G, s.card ≤ G.chromaticNumber.

Русский

Для клики s графа G выполняется s.card ≤ χ(G).

LaTeX

$$$|s| \le \chi(G)$$$

Lean4

/-- Given a colouring `α` of `G`, and a clique of size at least the number of colours, the clique
contains a vertex of each colour.
-/
theorem surjOn_of_card_le_isClique [Fintype α] {s : Finset V} (h : G.IsClique s) (hc : Fintype.card α ≤ s.card)
    (C : G.Coloring α) : Set.SurjOn C s Set.univ := by
  intro _ _
  obtain ⟨_, hx⟩ :=
    card_le_chromaticNumber_iff_forall_surjective.mp (by simp_all [isClique_iff_induce_eq])
      (C.comp (Embedding.induce s).toHom) _
  exact ⟨_, Subtype.coe_prop _, hx⟩

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