topologicalClosure — Mathlib

English

The topological closure of a subsemigroup is again a subsemigroup.

Русский

Топологическое замыкание подполугруппы опять является подполугруппой.

LaTeX

$$$s.topologicalClosure \text{ is a subsemigroup; } (\overline{S})\cdot(\overline{S}) \subseteq \overline{S}$$$

Lean4

/-- The (topological-space) closure of a subsemigroup of a space `M` with `ContinuousMul` is
itself a subsemigroup. -/
@[to_additive /-- The (topological-space) closure of an additive submonoid of a space `M` with
    `ContinuousAdd` is itself an additive submonoid. -/
    ]
def topologicalClosure (s : Subsemigroup M) : Subsemigroup M
    where
  carrier := _root_.closure (s : Set M)
  mul_mem' ha hb := s.top_closure_mul_self_subset ⟨_, ha, _, hb, rfl⟩

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