English
Let M be a semigroup with at least one element. For any finite cover s of M by subsets (i.e., ⊤ ⊆ ⋃₀ s), there exists a member c ∈ s and a FP-set a with FP a ⊆ c.
Русский
Пусть M — полугруппа с хотя бы одним элементом. Для любого конечного покрытия s M подмножествами (то есть ⊤ ⊆ ⋃₀ s) существует элемент c ∈ s и FP‑множество a такое, что FP a ⊆ c.
LaTeX
$$$$ \forall {M} [Semigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) (scov : \top \subseteq ⋃₀ s) : \exists c \in s, \exists a : Stream' M, FP a \subseteq c $$$$
Lean4
/-- The weak form of **Hindman's theorem**: in any finite cover of a nonempty semigroup, one of the
parts contains an FP-set. -/
@[to_additive exists_FS_of_finite_cover /-- The weak form of **Hindman's theorem**: in any finite
cover of a nonempty additive semigroup, one of the parts contains an FS-set. -/
]
theorem exists_FP_of_finite_cover {M} [Semigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) (scov : ⊤ ⊆ ⋃₀ s) :
∃ c ∈ s, ∃ a : Stream' M, FP a ⊆ c :=
let ⟨U, hU⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left (@Ultrafilter.continuous_mul_left M _)
let ⟨c, c_s, hc⟩ := (Ultrafilter.finite_sUnion_mem_iff sfin).mp (mem_of_superset univ_mem scov)
⟨c, c_s, exists_FP_of_large U hU c hc⟩
