English
G is n-partite if and only if it is colorable with n colors; equivalence between partitionable and colorable notions.
Русский
Граф G является n-разбиением тогда и только тогда, когда его можно раскрасить в n цветов; эквивалентности между двумя концепциями.
LaTeX
$$theorem partitionable_iff_colorable {n : ℕ} : G.Partitionable n ↔ G.Colorable n$$
Lean4
theorem partitionable_iff_colorable {n : ℕ} : G.Partitionable n ↔ G.Colorable n :=
by
constructor
· rintro ⟨P, hf, hc⟩
have : Fintype P.parts := hf.fintype
rw [Set.Finite.card_toFinset hf] at hc
apply P.colorable.mono hc
· rintro ⟨C⟩
refine ⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩
generalize_proofs h
change Set.Finite (Coloring.colorClasses C) at h
have : Fintype C.colorClasses := C.colorClasses_finite.fintype
rw [h.card_toFinset]
exact C.card_colorClasses_le
