English
Let M be a semigroup and a an FP-set generated by a stream. If FP a is covered by a finite family s of subsets, FP a ⊆ ⋃₀ s, then there exists c ∈ s and a FP-set b with FP b ⊆ c.
Русский
Пусть M — полугруппа и a — FP-множество, полученное из потока. Если FP a покрыто конечной семейство подмножеств s, то существует c ∈ s и FP‑множество b такое, что FP b ⊆ c.
LaTeX
$$$$ \forall \{M\} [Semigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) (scov : FP a ⊆ ⋃₀ s) : \exists c \in s, \exists b : Stream' M, FP b \subseteq c $$$$
Lean4
/-- The strong form of **Hindman's theorem**: in any finite cover of an FP-set, one the parts
contains an FP-set. -/
@[to_additive FS_partition_regular /-- The strong form of **Hindman's theorem**: in any finite
cover of an FS-set, one the parts contains an FS-set. -/
]
theorem FP_partition_regular {M} [Semigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite)
(scov : FP a ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ b : Stream' M, FP b ⊆ c :=
let ⟨U, idem, aU⟩ := exists_idempotent_ultrafilter_le_FP a
let ⟨c, cs, hc⟩ := (Ultrafilter.finite_sUnion_mem_iff sfin).mp (mem_of_superset aU scov)
⟨c, cs, exists_FP_of_large U idem c hc⟩
