normedSpace — Mathlib

English

A subspace inherits the norm from its ambient normed space by restriction.

Русский

Подпространство наследует норму исходного нормированного пространства по ограничению.

LaTeX

$$$\\|x\\|_{s} = \\|x\\|_{E} \\quad (x \\in s) $$$

Lean4

/-- A subspace of a normed space is also a normed space, with the restriction of the norm. -/
instance normedSpace {𝕜 R : Type*} [SMul 𝕜 R] [NormedField 𝕜] [Ring R] {E : Type*} [SeminormedAddCommGroup E]
    [NormedSpace 𝕜 E] [Module R E] [IsScalarTower 𝕜 R E] (s : Submodule R E) : NormedSpace 𝕜 s where
  norm_smul_le c x := norm_smul_le c (x : E)

Похожие утверждения