Theorems · Theorem · combinatorics

Hindman.FP_partition_regular

• 1000+ list: Hindman's theorem

∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (s : Set (Set M)),
  s.Finite → Hindman.FP a ⊆ ⋃₀ s → ∃ c ∈ s, ∃ b, Hindman.FP b ⊆ c

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

Defined in

Mathlib.Combinatorics.Hindman

Cited by

0 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semigroup