Theorems · Definition · Lie groups

Subsemigroup.topologicalClosure

{M : Type u_3} →
  [inst : TopologicalSpace M] → [inst_1 : Semigroup M] → [SeparatelyContinuousMul M] → Subsemigroup M → Subsemigroup M

The (topological-space) closure of a subsemigroup of a space M with ContinuousMul is itself a subsemigroup.

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

5 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceSemigroupSeparatelyContinuousMul