English
If a topological space α carries a continuous scalar action by a semiring R, then restricting the scalars to nonnegative elements {r ∈ R | 0 ≤ r} yields a continuous scalar action on α. In particular, the map (r, a) ↦ r • a is continuous for r ≥ 0.
Русский
Если на топологическом пространстве α задано непрерывное скалярное умножение на полуруслование R, то ограничение скаляров до неположительных элементов {r ∈ R | 0 ≤ r} сохраняет непрерывность действия, то есть отображение (r, a) ↦ r • a непрерывно.
LaTeX
$$$\\forall R, \\alpha \\, [\\text{Semiring } R] [\\text{PartialOrder } R] [\\text{SMul } R \\alpha] [\\text{TopologicalSpace } \\alpha] \\, [\\text{ContinuousConstSMul } R \\alpha], \\, \\text{ContinuousConstSMul} \\{ r : R \\mid 0 \\le r \\} \\alpha$$$
Lean4
instance [ContinuousConstSMul R α] : ContinuousConstSMul { r : R // 0 ≤ r } α where
continuous_const_smul r := continuous_const_smul r.1
