topologicalClosure — Mathlib

English

Let R be a nonunital topological ring and S a nonunital subring of R. Then the topological closure of S in R is again a nonunital subring of R.

Русский

Пусть R — неполное топологическое кольцо, и S — неполное подкольцо R. Тогда топологическое замыкание S в R снова является неполным подкольцом R.

LaTeX

$$$\overline{S} \text{ is a nonunital subring of } R$$$

Lean4

/-- The (topological) closure of a non-unital subring of a non-unital topological ring is
itself a non-unital subring. -/
def topologicalClosure (S : NonUnitalSubring R) : NonUnitalSubring R :=
  { S.toSubsemigroup.topologicalClosure, S.toAddSubgroup.topologicalClosure with carrier := _root_.closure (S : Set R) }

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