English
Let R be a topological semiring, s a subsemiring of R, and X a topological space with an action of R on X such that the action map R × X → X is continuous. Then the restricted action of s on X is continuous; i.e., the map s × X → X given by (a, x) ↦ a • x is continuous.
Русский
Пусть R — топологическое полукольцо, s — подполукольцо R, X — топологическое пространство с действием R на X, и это действие непрерывно. Тогда ограниченное действие s на X непрерывно: отображение s × X → X, (a, x) ↦ a • x непрерывно.
LaTeX
$$$\\forall \\ R [TopologicalSpace\ investigates R] [Semiring R] [IsTopologicalSemiring R] (s : Subsemiring R) (X : Type) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X],\\; ContinuousSmul (s) (X)$$$
Lean4
instance continuousSMul (s : Subsemiring R) (X) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X] :
ContinuousSMul s X :=
Submonoid.continuousSMul
