top_closure_mul_self_eq — Mathlib

English

The product of closures equals the closure for Submonoid: closure(S) · closure(S) = closure(S).

Русский

Произведение замыканий равно их замыканию: closure(S)·closure(S) = closure(S).

LaTeX

$$closure (S) * closure (S) = closure (S)$$

Lean4

@[to_additive]
theorem top_closure_mul_self_eq (s : Submonoid M) : _root_.closure (s : Set M) * _root_.closure s = _root_.closure s :=
  Subset.antisymm s.top_closure_mul_self_subset fun x hx => ⟨x, hx, 1, _root_.subset_closure s.one_mem, mul_one _⟩

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