topologicalSemiring

Mathlib.Topology.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#Subsemiring.topologicalSemiring

English

A topological structure on a subsemiring is inherited from the ambient ring’s topology.

Русский

Топологическая структура подпол semiring наследуется от окружения кольца.

LaTeX

$$$\\mathrm{IsTopologicalSemiring}(\\text{Subsemiring}(R))$$$

Lean4

instance topologicalSemiring (S : Subsemiring R) : IsTopologicalSemiring S :=
  { S.toSubmonoid.continuousMul, S.toAddSubmonoid.continuousAdd with }

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

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

Разделы

Аффилиация

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