exists_multiset_of_mem_closure — Mathlib

English

If x ∈ closure(s) in a commutative monoid, there exists a multiset of elements from s whose product equals x.

Русский

Если x ∈ closure(s) в коммутативном моноиде, то существует мультисет элементов из s, произведение которых равно x.

LaTeX

$$$\\exists l : \\mathrm{Multiset}\, M, (\\forall y \\in l, y \\in s) \\land l.prod = x$$$

Lean4

@[to_additive]
theorem exists_multiset_of_mem_closure {M : Type*} [CommMonoid M] {s : Set M} {x : M} (hx : x ∈ closure s) :
    ∃ l : Multiset M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x :=
  by
  obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
  exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

Похожие утверждения