English
The Hales–Jewett theorem: for any finite α and κ, there exists a finite index set ι such that for every coloring C: ι→α → κ there exists a Line α ι that is mono for C.
Русский
Теорема Хейлса–Дьюэта: для любых конечных α и κ существует конечный индекс ι так, что для каждого раскраски C : ι → α → κ существует_Line α ι, моно относительно C.
LaTeX
$$$\\exists ι\\ (Fintype\\ ι)\\ ,\\forall C:(ι\\to α)\\to κ,\\exists l:Line\\ α\\ ι,\\ IsMono\\ C\\ l$$$
Lean4
/-- The **Hales-Jewett theorem**: For any finite types `α` and `κ`, there exists a finite type `ι`
such that whenever the hypercube `ι → α` is `κ`-colored, there is a monochromatic combinatorial
line. -/
theorem exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] :
∃ (ι : Type) (_ : Fintype ι), ∀ C : (ι → α) → κ, ∃ l : Line α ι, l.IsMono C :=
let ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension'.{u, v} α (ULift.{u, v} κ)
⟨ι, ιfin, fun C =>
let ⟨l, c, hc⟩ := hι (ULift.up ∘ C)
⟨l, c.down, fun x => by rw [← hc x, Function.comp_apply]⟩⟩
