Email Gateway (Sep 07 2022 at 09:16): Email Gateway (Sep 07 2022 at 09:16):From: Tobias Nipkow <nipkow@in.tum.de>
The Hales-Jewett Theorem
Ujkan Sulejmani, Manuel Eberl and Katharina Kreuzer
Abstract
This article is a formalisation of a proof of the Hales--Jewett theorem
presented in the textbook Ramsey Theory by Graham et al.
The Hales--Jewett theorem is a result in Ramsey Theory which states that, for
any non-negative integers r
and t, there exists a minimal dimension N, such that any r-coloured
N'-dimensional cube over t elements (with N' >= N) contains a monochromatic
line. This theorem generalises Van der Waerden's Theorem, which has already been
formalised in another AFP entry.
https://www.isa-afp.org/entries/Hales_Jewett.html
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC