instIsTopologicalSemiringSubtypeMemSubalgebra

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#instIsTopologicalSemiringSubtypeMemSubalgebra

English

The topological closure of a subalgebra inherits a topological semiring structure.

Русский

Замыкание сверху подалгебры наследует структуру топологического полупрямоугольника (семиринга).

LaTeX

$$$\text{IsTopologicalSemiring}(s_{topologicalClosure})$$$

Lean4

instance (s : Subalgebra R A) : IsTopologicalSemiring s :=
  s.toSubsemiring.topologicalSemiring

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru