English
Every n-colorable graph G, with color classes of size at most t, can be embedded into the complete equipartite graph with n parts and part size t.
Русский
Каждый граф G, цветовой класс которого можно разбить на n цветов с размером каждого класса не более t, можно вложить в граф K_n(t).
LaTeX
$$GColoring : Fin n → G.Coloring (Fin n) with colorClass sizes ≤ t ⇒ G ⊑ completeEquipartiteGraph n t$$
Lean4
/-- Every `n`-colorable graph is contained in a `completeEquipartiteGraph` in `n` parts (as long
as the parts are at least as large as the largest color class). -/
theorem isContained_completeEquipartiteGraph_of_colorable {n : ℕ} (C : G.Coloring (Fin n)) (t : ℕ)
(h : ∀ c, card (C.colorClass c) ≤ t) : G ⊑ completeEquipartiteGraph n t :=
by
have (c : Fin n) : Nonempty (C.colorClass c ↪ Fin t) :=
by
rw [Function.Embedding.nonempty_iff_card_le, Fintype.card_fin]
exact h c
have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)
have hF {c₁ c₂ v₁ v₂} (hc : c₁ = c₂) (hv : F c₁ v₁ = F c₂ v₂) : v₁.val = v₂.val :=
by
let v₁' : C.colorClass c₂ := ⟨v₁, by simp [← hc]⟩
have hv' : F c₁ v₁ = F c₂ v₁' := by
apply congr_heq
· rw [hc]
· rw [Subtype.heq_iff_coe_eq]
simp [hc]
rw [hv'] at hv
simpa [Subtype.ext_iff] using (F c₂).injective hv
use ⟨fun v ↦ (C v, F (C v) ⟨v, C.mem_colorClass v⟩), C.valid⟩
intro v w h
rw [Prod.mk.injEq] at h
exact hF h.1 h.2
