English
In a commutative monoid M, an element x lies in the closure of a subset s if and only if there exist a function f: M → ℕ and a finite set t ⊆ M such that the support of f is contained in t, t ⊆ s, and the product over t of a^{f(a)} equals x.
Русский
В коммутативном моноиде M элемент x принадлежит замыканию множества s тогда и только тогда, когда существуют функция f: M → ℕ и конечное подмножество t ⊆ M such that поддержка f ⊆ t, t ⊆ s, и ∏_{a∈t} a^{f(a)} = x.
LaTeX
$$$$ x \\in \\overline{s} \\iff \\exists f:M\\to\\mathbb{N}\\,\\exists t:\\Finset M, \\ t\\subseteq s \\land f\\_support \\subseteq t \\land \\prod_{a\\in t} a^{f(a)} = x $$$$
Lean4
@[to_additive]
theorem mem_closure_iff_exists_finset_subset {s : Set M} :
x ∈ closure s ↔ ∃ (f : M → ℕ) (t : Finset M), ↑t ⊆ s ∧ f.support ⊆ t ∧ ∏ a ∈ t, a ^ f a = x
where
mp
hx := by
classical
induction hx using closure_induction with
| one => exact ⟨0, ∅, by simp⟩
| mem x hx =>
simp only at hx
exact ⟨Pi.single x 1, { x }, by simp [hx, Pi.single_apply]⟩
| mul x y _ _ hx hy =>
obtain ⟨f, t, hts, hf, rfl⟩ := hx
obtain ⟨g, u, hus, hg, rfl⟩ := hy
refine
⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
(Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
congr 1 <;> symm
· refine Finset.prod_subset Finset.subset_union_left ?_
simp +contextual [Function.support_subset_iff'.1 hf]
· refine Finset.prod_subset Finset.subset_union_right ?_
simp +contextual [Function.support_subset_iff'.1 hg]
mpr := by rintro ⟨n, t, hts, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure <| hts hx) _
