English
A finite-index version of the extended Hales-Jewett theorem: there exists a finite n such that for every C: Fin n → α → κ there is a Subspace of dimension η in α^{Fin n} that is monochromatic for C.
Русский
Версия Хейла–Жуэтта с конечной размерностью: существует n, такое что для любого отображения окраски C: Fin n → α → κ существует подпространство размерности η внутри α^{Fin n}, на котором C монохромно.
LaTeX
$$$\\\\exists n \\\\text{ such that } \\\\forall C:(\\\\mathrm{Fin}\ n \\\\to \\\\alpha) \\\\to \\\\kappa,\n\\\\exists l:\\\\text{Subspace}_{\\\\eta}(\\\\alpha,\\\\mathrm{Fin}\,n),\\\\text{l.IsMono}(C).$$$
Lean4
/-- A variant of the **extended Hales-Jewett theorem** `exists_mono_in_high_dimension` where the
returned type is some `Fin n` instead of a general fintype. -/
theorem exists_mono_in_high_dimension_fin (α κ η) [Finite α] [Finite κ] [Finite η] :
∃ n, ∀ C : (Fin n → α) → κ, ∃ l : Subspace η α (Fin n), l.IsMono C :=
by
obtain ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension α κ η
refine ⟨Fintype.card ι, fun C ↦ ?_⟩
obtain ⟨l, c, cl⟩ := hι fun v ↦ C (v ∘ (Fintype.equivFin _).symm)
refine ⟨⟨l.idxFun ∘ (Fintype.equivFin _).symm, fun e ↦ ?_⟩, c, cl⟩
obtain ⟨i, hi⟩ := l.proper e
use Fintype.equivFin _ i
simpa using hi
