le_chromaticNumber_iff_forall_surjective

English

For any natural n, n ≤ χ(G) if and only if every coloring of Fin n is surjective.

Русский

Для любого натурального n, n ≤ χ(G) тогда и только тогда каждая раскраска Fin n является сюръективной.

LaTeX

$$n ≤ G.chromaticNumber ↔ ∀ C : G.Coloring (Fin n), Surjective C$$

Lean4

theorem le_chromaticNumber_iff_forall_surjective : n ≤ G.chromaticNumber ↔ ∀ C : G.Coloring (Fin n), Surjective C := by
  simp [← card_le_chromaticNumber_iff_forall_surjective]

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