subset_closure — Mathlib

English

For any subset s of a magma M, the set s is contained in its closure under the semigroup operation.

Русский

Для любого подмножества s множества M, сам s содержится в its closure (замыкании) относительно операции умножения.

LaTeX

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

Lean4

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

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