Theorems · Definition · Lie groups

Submonoid.topologicalClosure

{M : Type u_3} →
  [inst : TopologicalSpace M] → [inst_1 : Monoid M] → [SeparatelyContinuousMul M] → Submonoid M → Submonoid M

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

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMonoidSeparatelyContinuousMul