Theorems · Definition · Lie groups

AddSubmonoid.topologicalClosure

{M : Type u_3} →
  [inst : TopologicalSpace M] → [inst_1 : AddMonoid M] → [SeparatelyContinuousAdd M] → AddSubmonoid M → AddSubmonoid M

The (topological-space) closure of an additive submonoid of a space M with ContinuousAdd is itself an additive 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

TopologicalSpaceAddMonoidSeparatelyContinuousAdd