Ramsey theory

TheoremVan der Waerden theorem#

A generalization of Van der Waerden's theorem: if M is a finitely colored commutative monoid, and S is a finite subset, then there exists a monochromatic homothetic copy of S.

Combinatorics.exists_mono_homothetic_copy.{u_5, u_6} {M : Type u_5} {κ : Type u_6} [AddCommMonoid M]
  (S : Finset M) [Finite κ] (C : M → κ) : ∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
Sources
MathlibCombinatorics.exists_mono_homothetic_copy
Uses 3
Statement usesFinite set · Natural number
Proof usesHales-Jewett theorem

TheoremHales-Jewett theorem#

The Hales-Jewett theorem: For any finite types α and κ, there exists a finite type ι such that whenever the hypercube ι → α is κ-colored, there is a monochromatic combinatorial line.

Combinatorics.Line.exists_mono_in_high_dimension.{u, v} (α : Type u) [Finite α] (κ : Type v)
  [Finite κ] : ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Line.IsMono C l
Sources
MathlibCombinatorics.Line.exists_mono_in_high_dimension
Uses 2 · Used by 1
Statement usesFinite set · Natural number
Used byVan der Waerden theorem

TheoremHindman's theorem (Ramsey theory)#

The strong form of Hindman's theorem: in any finite cover of an FS-set, one the parts contains an FS-set.

Hindman.FS_partition_regular.{u_1} {M : Type u_1} [AddSemigroup M] (a : Stream' M) (s : Set (Set M))
  (sfin : s.Finite) (scov : ∀ (m : M), Hindman.FS a m → m ∈ ⋃₀ s) :
  ∃ c ∈ s, ∃ b, ∀ (m : M), Hindman.FS b m → m ∈ c
Sources
MathlibHindman.FS_partition_regular
Uses 4
Statement usesStream
Proof usesCompactness in terms of filters · Continuous function · Hausdorff space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.