English
If R is a topological semiring and M is a topological R-module with continuous scalar actions and addition, then tsze R M is a topological semiring.
Русский
Если R — топологическое полугруппа-набор, а M — топологический R-модуль с непрерывными скалярами и сложением, то tsze R M является топологическим полугруппой по умножению.
LaTeX
$$$\\operatorname{IsTopologicalSemiring}(\\mathrm{tsze}(R,M))$$$
Lean4
/-- This is not an instance due to complaints by the `fails_quickly` linter. At any rate, we only
really care about the `IsTopologicalRing` instance below. -/
theorem topologicalSemiring [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] [IsTopologicalSemiring R]
[ContinuousAdd M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] : IsTopologicalSemiring (tsze R M) :=
{ }
