top_closure_mul_self_subset — Mathlib

English

For a Submonoid S in a topological monoid M, the product of the closures of S with itself is contained in the closure of S.

Русский

Для подмоноида S внутри топологического моноида M произведение замыкания S с самим собой содержится в замыкании S.

LaTeX

$$closure (S) * closure (S) ⊆ closure (S)$$

Lean4

@[to_additive]
theorem top_closure_mul_self_subset (s : Submonoid M) :
    _root_.closure (s : Set M) * _root_.closure s ⊆ _root_.closure s :=
  image2_subset_iff.2 fun _ hx _ hy => map_mem_closure₂ continuous_mul hx hy fun _ ha _ hb => s.mul_mem ha hb

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