English
The underlying set of the topologicalClosure of a Submonoid is the closure of the underlying set.
Русский
Подмножество, лежащее в основе topologicalClosure подмножества, равно замыканию исходного множества.
LaTeX
$$(s.topologicalClosure : Set M) = closure (s : Set M)$$
Lean4
/-- The (topological-space) closure of a submonoid of a space `M` with `ContinuousMul` is
itself a submonoid. -/
@[to_additive /-- The (topological-space) closure of an additive submonoid of a space `M` with
`ContinuousAdd` is itself an additive submonoid. -/
]
def topologicalClosure (s : Submonoid M) : Submonoid M
where
carrier := _root_.closure (s : Set M)
one_mem' := _root_.subset_closure s.one_mem
mul_mem' ha hb := s.top_closure_mul_self_subset ⟨_, ha, _, hb, rfl⟩
