English
Let M be a magma and s a subset of M. The subsemigroup generated by s is the smallest subsemigroup containing s; equivalently, an element x lies in closure(s) if and only if x lies in every subsemigroup of M that contains s.
Русский
Пусть M — множество с операцией умножения (мagma), и s — подмножество M. Подполугруппа, порождаемая s, является наименьшей подполугруппой, содержащей s; эквивалентно, элемент x принадлежит closure(s) тогда и только тогда, когда x принадлежит каждой подполугруппе M, содержащей s.
LaTeX
$$$ x \\in \\langle s \\rangle \\;\\iff\\; \\forall S : \\mathrm{Subsemigroup}\\, M,\\ s \\subseteq S \\Rightarrow x \\in S $$$
Lean4
@[to_additive]
theorem mem_closure {x : M} : x ∈ closure s ↔ ∀ S : Subsemigroup M, s ⊆ S → x ∈ S :=
mem_sInf
