English
If f is a linear map from a module to a normed space, then the domain can be given a normed-space structure induced by f, with the norm bound ||a•x|| ≤ ||a|| · ||f(x)|| for all a, x.
Русский
Если f — линейное отображение между модулем и нормированным пространством, то область определения может быть снабжена нормированным пространством, индуцированным через f, так что для всех a, x выполняется неравенство ||a • x|| ≤ ||a|| · ||f(x)||.
LaTeX
$$$\\text{induced} \\; (f) := \\bigl( x \\mapsto \\|f(x)\\| \\bigr) \\quad \\Rightarrow\\quad \\|a \\cdot x\\| \\le \\|a\\| \\cdot \\|f(x)\\|$$
Lean4
instance (priority := 100) toNormSMulClass [NormedSpace 𝕜 E] : NormSMulClass 𝕜 E :=
haveI : IsBoundedSMul 𝕜 E := .of_norm_smul_le NormedSpace.norm_smul_le
NormedDivisionRing.toNormSMulClass
