English
If a scalar action of R on M is given byContinuousConstSMul, then the same action induces a canonical action on the function space C(α, M) by pointwise multiplication: (r • f)(x) = r • f(x), and this operation is continuous in the appropriate sense.
Русский
Пусть на множестве M задана скаляционная операция атомарного типа R, и имеется непрерывное постоянное умножение на скаляр, тогда на пространстве непрерывных функций C(α, M) действует аналогичная операция по точке: (r • f)(x) = r • f(x), и эта операция непрерывная в соответствующем смысле.
LaTeX
$$$ (r \cdot f)(x) = r \cdot f(x) \quad \text{для всех } x. $$$
Lean4
@[to_additive]
instance [SMul R M] [ContinuousConstSMul R M] : ContinuousConstSMul R C(α, M) where
continuous_const_smul r := continuous_postcomp ⟨_, continuous_const_smul r⟩
