English
For finite color sets α, card α ≤ chromaticNumber if and only if every coloring α is surjective.
Русский
Для конечного множества цветов α, card α ≤ χ(G) тогда и только тогда любой раскраской C: GColoring α является сюръективной.
LaTeX
$$[Fintype α] : card α ≤ G.chromaticNumber ↔ ∀ C : G.Coloring α, Surjective C$$
Lean4
theorem card_le_chromaticNumber_iff_forall_surjective [Fintype α] :
card α ≤ G.chromaticNumber ↔ ∀ C : G.Coloring α, Surjective C :=
by
refine ⟨fun h C ↦ ?_, fun h ↦ ?_⟩
· rw [C.colorable.chromaticNumber_eq_sInf, Nat.cast_le] at h
intro i
by_contra! hi
let D : G.Coloring { a // a ≠ i } := ⟨fun v ↦ ⟨C v, hi v⟩, (C.valid · <| congr_arg Subtype.val ·)⟩
classical
exact
Nat.notMem_of_lt_sInf ((Nat.sub_one_lt_of_lt <| card_pos_iff.2 ⟨i⟩).trans_le h)
⟨G.recolorOfEquiv (equivOfCardEq <| by simp) D⟩
· simp only [chromaticNumber, Set.mem_setOf_eq, le_iInf_iff, Nat.cast_le]
rintro i ⟨C⟩
contrapose! h
refine ⟨G.recolorOfCardLE (by simpa using h.le) C, fun hC ↦ ?_⟩
dsimp at hC
simpa [h.not_ge] using Fintype.card_le_of_surjective _ hC.of_comp
