subset_closure — Mathlib

English

The submonoid generated by a set always contains that set: s ⊆ closure(s).

Русский

Подмономоид, порожденный множестом, всегда содержит это множество: s ⊆ closure(s).

LaTeX

$$$ s \\subseteq \\operatorname{closure}(s) $$$

Lean4

/-- The submonoid generated by a set includes the set. -/
@[to_additive (attr := simp, aesop safe 20 (rule_sets := [SetLike])) /--
    The `AddSubmonoid` generated by a set includes the set. -/
    ]
theorem subset_closure : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx

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