instIsTopologicalSemiring — Mathlib

English

The topological closure of the image under a star map equals the image of the topological closure under suitable assumptions.

Русский

Топологическое замыкание образа под звездным отображением равно образу топологического замыкания при подходящих условиях.

LaTeX

$$$\overline{\operatorname{map}_φ(S)} = \operatorname{map}_φ(\overline{S})$$$

Lean4

instance instIsTopologicalSemiring (s : NonUnitalStarSubalgebra R A) : IsTopologicalSemiring s :=
  s.toNonUnitalSubalgebra.instIsTopologicalSemiring

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