coe_topologicalClosure — Mathlib

English

The underlying set of the topologicalClosure of a subsemigroup equals the closure of the underlying set of the subsemigroup.

Русский

Множество, лежащее в основе topologicalClosure подполугруппы, равно замыканию множества самой подполугруппы.

LaTeX

$$$(s.topologicalClosure : Set M) = \overline{(s : Set M)}$$

Lean4

@[to_additive]
theorem coe_topologicalClosure (s : Subsemigroup M) : (s.topologicalClosure : Set M) = _root_.closure (s : Set M) :=
  rfl

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