Commit 2024-07-23 15:36 127e9c5e

View on Github →

feat: Combinatorial subspaces and multidimensional Hales-Jewett (#8304) This PR extends the Hales-Jewett theorem from combinatorial lines to higher-dimensional combinatorial subspaces. It's an example of a theorem proving its own generalisation.

Estimated changes

Modified Mathlib/Combinatorics/HalesJewett.lean

deleted theorem Combinatorics.Line.apply

added theorem Combinatorics.Line.apply_def

deleted theorem Combinatorics.Line.apply_of_ne_none

added theorem Combinatorics.Line.apply_some

added theorem Combinatorics.Line.coe_apply

added theorem Combinatorics.Line.coe_injective

added def Combinatorics.Line.toFun

added def Combinatorics.Line.toSubspace

added def Combinatorics.Line.toSubspaceUnit

added theorem Combinatorics.Line.toSubspaceUnit_apply

added theorem Combinatorics.Line.toSubspaceUnit_isMono

added theorem Combinatorics.Line.toSubspace_apply

added theorem Combinatorics.Line.toSubspace_isMono

added def Combinatorics.Subspace.IsMono

added theorem Combinatorics.Subspace.apply_def

added theorem Combinatorics.Subspace.apply_inl

added theorem Combinatorics.Subspace.apply_inr

added theorem Combinatorics.Subspace.coe_apply

added theorem Combinatorics.Subspace.coe_injective

added theorem Combinatorics.Subspace.exists_mono_in_high_dimension

added theorem Combinatorics.Subspace.exists_mono_in_high_dimension_fin

added def Combinatorics.Subspace.reindex

added theorem Combinatorics.Subspace.reindex_apply

added theorem Combinatorics.Subspace.reindex_isMono

added def Combinatorics.Subspace.toFun

added structure Combinatorics.Subspace