English
A Submodule S of E, with the inherited structure, is a normed space.
Русский
У подпространства S пространства E с унаследованной структурой есть норма как в нормированном пространстве.
LaTeX
$$$\\text{NormedSpace } 𝕜 S$ with restricted norm$$
Lean4
/-- A linear map from a `Module` to a `NormedSpace` induces a `NormedSpace` structure on the
domain, using the `SeminormedAddCommGroup.induced` norm.
See note [reducible non-instances] -/
abbrev induced {F : Type*} (𝕜 E G : Type*) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [SeminormedAddCommGroup G]
[NormedSpace 𝕜 G] [FunLike F E G] [LinearMapClass F 𝕜 E G] (f : F) :
@NormedSpace 𝕜 E _ (SeminormedAddCommGroup.induced E G f) :=
let _ := SeminormedAddCommGroup.induced E G f
⟨fun a b ↦ by simpa only [← map_smul f a b] using norm_smul_le a (f b)⟩
