English
For a finite set s in a commutative monoid M, an element x lies in the closure of s iff there exists a function f with support in s such that the product over s of a^{f(a)} equals x.
Русский
Для конечного множества s в коммутативном моноиде M элемент x принадлежит замыканию s тогда и только тогда, когда существует функция f с опорой в s, такая что произведение по a∈s a^{f(a)} равно x.
LaTeX
$$$$ x \\in \\overline{s} \\iff \\exists f:M \\to \\mathbb{N}, f.{\\scriptsize\\mathrm{support}} \\subseteq s \\land \\prod_{a \\in s} a^{f(a)} = x $$$$
Lean4
@[to_additive]
theorem mem_closure_finset {s : Finset M} : x ∈ closure s ↔ ∃ f : M → ℕ, f.support ⊆ s ∧ ∏ a ∈ s, a ^ f a = x
where
mp := by
rw [mem_closure_iff_exists_finset_subset]
rintro ⟨f, t, hts, hf, rfl⟩
refine ⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩
simp +contextual [Function.support_subset_iff'.1 hf]
mpr := by rintro ⟨n, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure hx) _
