top_closure_mul_self_subset — Mathlib

English

For any subsemigroup s of a topological semigroup M with continuous multiplication, the product of its closure with itself is contained in the closure of s.

Русский

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

LaTeX

$$$\overline{s}\cdot\overline{s} \subseteq \overline{s}$$$

Lean4

@[to_additive]
theorem top_closure_mul_self_subset (s : Subsemigroup 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

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