English
Let V, V1, V2, V3 be seminormed additive groups and f, g be normed additive group homomorphisms from V1 to V2. If R is a semiring with a compatible R-module structure on V2 and a bounded scalar action, then the set of all NormedAddGroupHom(V1, V2) carries a natural structure of an R-module, with (r · f)(x) = r · (f(x)).
Русский
Пусть V, V1, V2, V3 — полугруппы с нормой (полуметрическое пространство), а f, g — гомоморфизмы нормированной аддитивной группы из V1 в V2. Если R — полурумьевая структура с совместимой R-модульностью на V2 и ограниченным скалярным умножением, тогда множество NormedAddGroupHom(V1, V2) естественно является модулем над R, причем (r · f)(x) = r · (f(x)).
LaTeX
$$$\\operatorname{NormedAddGroupHom}(V_1,V_2)$ имеет естественную структуру модуля над $R$; для $r\\in R$, $f:\\ V_1\\to V_2$ и $x\\in V_1$ выполняется $(r\\cdot f)(x)=r\\cdot f(x)$.$$
Lean4
instance module {R : Type*} [Semiring R] [Module R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] :
Module R (NormedAddGroupHom V₁ V₂) :=
Function.Injective.module _ coeAddHom coe_injective coe_smul
