chromaticNumber_eq_card_iff_forall_surjective

English

If G is colorable with card α colors, then χ(G) = card α if and only if every coloring α is surjective.

Русский

Если граф окрашен в card α цветов, то χ(G) = card α тогда и только тогда каждая раскраска α — сюръективна.

LaTeX

$$G.Colorable (card α) → (G.chromaticNumber = card α ↔ ∀ C : G.Coloring α, Surjective C)$$

Lean4

theorem chromaticNumber_eq_card_iff_forall_surjective [Fintype α] (hG : G.Colorable (card α)) :
    G.chromaticNumber = card α ↔ ∀ C : G.Coloring α, Surjective C := by
  rw [← hG.chromaticNumber_le.ge_iff_eq, card_le_chromaticNumber_iff_forall_surjective]

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