topologicalClosure — Mathlib

English

The topological closure of a subsemiring s of a topological semiring R is again a subsemiring of R.

Русский

Топологическое замыкание подполукольца s внутри топологического полукольца R снова образует подполукольцо.

LaTeX

$$$\\operatorname{topologicalClosure}(s) \\in \\text{Subsemiring}(R)$$$

Lean4

/-- The (topological-space) closure of a subsemiring of a topological semiring is
itself a subsemiring. -/
def topologicalClosure (s : Subsemiring R) : Subsemiring R :=
  { s.toSubmonoid.topologicalClosure, s.toAddSubmonoid.topologicalClosure with carrier := _root_.closure (s : Set R) }

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