Existing in Mathlib · Combinatorics
Hales–Jewett Theorem
Fix a finite alphabet and finitely many colors. In some sufficiently large finite word space, no matter how every word is colored, there is a family of words obtained by changing one nonempty set of positions together, all with the same color.
- Ramsey theory
- finite word hypercubes
- combinatorial lines
- finite colorings
- color focusing
- product argument
Exact theorem
Exact Mathlib statement
theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] : ∃ (ι : Type) (_ : Fintype ι), ∀ C : (ι → α) → κ, ∃ l : Combinatorics.Line α ι, l.IsMono CThe theorem at a glance
Hales–Jewett Theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Hales–Jewett Theorem at a glance
Detailed visual description
The theorem block preserves the finite alphabet and color hypotheses, existential finite coordinate type, universal coloring, and monochromatic-line conclusion. The central example gives the complete line for alphabet {a,b,c} under the pattern (a,x,x,b,x): (a,a,a,b,a), (a,b,b,b,b), and (a,c,c,b,c), all with one whole-word halo. The footer explicitly records the non-effective and one-dimensional boundary.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
A monochromatic combinatorial line — Scientific schematic
Detailed visual description
Three outlined five-tile words appear one above another. The first and fourth columns contain the same cobalt circle and emerald diamond in every row. Columns two, three, and five all show circles in the first row, diamonds in the second, and six-pointed gold stars in the third. These are all three letters of the same alphabet, including both fixed letters. Identical vermilion outlines represent one common whole-word color. The faint background lattice is decorative context. This five-coordinate example illustrates a combinatorial line; it does not claim that dimension five suffices for an arbitrary coloring in the Hales–Jewett theorem.
Why it matters
A mathematical landmark
The Hales–Jewett theorem is a central structural result in Ramsey theory. Mathlib’s source exposes the theorem’s distinctive route through induction on the alphabet, color-focused families, a product argument, and the final impossibility of more distinct focused colors than the finite color type contains.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib’s combinatorial-line form of the Hales–Jewett theorem for arbitrary finite types α and κ. It produces some finite coordinate type ι before quantifying over every coloring C : (ι → α) → κ. A line fixes some coordinates and varies one nonempty set of coordinates together through a common letter. The selected declaration supplies no effective or least dimension, canonical choice, coloring-independent line, or algorithm, and it is not the separate multidimensional subspace theorem or the Van der Waerden corollary.
- ProofAtlas did not originate the Hales–Jewett theorem or Mathlib’s declaration.
- The selected declaration gives no effective upper bound or least value for the finite coordinate dimension.
- The displayed five-coordinate line is an illustration, not a universally sufficient Hales–Jewett dimension.
- The selected declaration is not the separate multidimensional Hales–Jewett theorem and does not itself state Van der Waerden’s theorem.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Combinatorics.Line.exists_mono_in_high_dimensionin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.hales-jewett-theorem.v001