Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-17 19:58 ad5afc21

View on Github →

feat(combinatorics/hales_jewett): Hales-Jewett and Van der Waerden (#8019) Proves the Hales-Jewett theorem (a fundamental result in Ramsey theory on combinatorial lines) and deduces (a generalised version of) Van der Waerden's theorem on arithmetic progressions.

Estimated changes

Created src/combinatorics/hales_jewett.lean

added theorem combinatorics.exists_mono_homothetic_copy

added structure combinatorics.line.almost_mono

added theorem combinatorics.line.apply

added theorem combinatorics.line.apply_none

added theorem combinatorics.line.apply_of_ne_none

added structure combinatorics.line.color_focused

added def combinatorics.line.diagonal

added theorem combinatorics.line.diagonal_apply

added theorem combinatorics.line.exists_mono_in_high_dimension

added def combinatorics.line.horizontal

added theorem combinatorics.line.horizontal_apply

added def combinatorics.line.is_mono

added def combinatorics.line.map

added theorem combinatorics.line.map_apply

added def combinatorics.line.prod

added theorem combinatorics.line.prod_apply

added def combinatorics.line.vertical

added theorem combinatorics.line.vertical_apply

added structure combinatorics.line

Modified src/data/list/basic.lean

Modified src/data/option/basic.lean

added theorem option.get_or_else_map

added theorem option.get_or_else_none