exists_list_of_mem_closure — Mathlib

English

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

Русский

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

LaTeX

$$$\\exists l : List M, (\\forall y \\in l, y \\in s) \\land l.prod = x$$$

Lean4

@[to_additive]
theorem exists_list_of_mem_closure {s : Set M} {x : M} (hx : x ∈ closure s) :
    ∃ l : List M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x := by
  rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

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