English
Let α, κ, η be finite types. There exists a finite index set ι such that for every κ-coloring C of the hypercube ι → α there is a monochromatic combinatorial subspace of dimension η.
Русский
Пусть α, κ, η — конечные множества. Существует конечный индексный множество ι such that для любого κ-окрашивания гиперкуба ι → α существует монохроматное комбинаторное подпространство размерности η.
LaTeX
$$$\\\\forall \\\\alpha,\\\\kappa,\\\\eta \\\\text{finite},\\\\exists \\\\iota \\\\text{finite},\\\\forall C:(\\\\iota \\\\to \\\\alpha) \\\\to \\\\kappa,\\\\exists l:\\\\text{Subspace}_{\\\\eta}(\\\\alpha,\\\\iota),\\\\text{l.IsMono}(C).$$$
Lean4
/-- The **multidimensional Hales-Jewett theorem**, aka **extended 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 subspace of dimension `η`. -/
theorem exists_mono_in_high_dimension (α κ η) [Finite α] [Finite κ] [Finite η] :
∃ (ι : Type) (_ : Fintype ι), ∀ C : (ι → α) → κ, ∃ l : Subspace η α ι, l.IsMono C :=
by
cases nonempty_fintype η
obtain ⟨ι, _, hι⟩ := Line.exists_mono_in_high_dimension (Shrink.{0} η → α) κ
refine ⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩
obtain ⟨l, hl⟩ := hι fun x ↦ C fun (i, e) ↦ x i e
refine ⟨l.toSubspace.reindex (equivShrink.{0} η).symm (Equiv.refl _) (Equiv.refl _), ?_⟩
convert hl.toSubspace.reindex
simp
