instNormedSpaceSubtypeMemAddSubgroupSelfAdjointOfTrivialStarOfStarModule

English

Under suitable Star and normed-module assumptions, the set of self-adjoint elements forms a normed space when restricted to a real structure, i.e., the self-adjoint elements carry a compatible normed-space structure.

Русский

При надлежащих предположениях о звезде и нормированном модуле множество самосопряжённых элементов образует нормированное линейное пространство.

LaTeX

$$$\text{SelfAdjoint}(E) \text{ inherits a normed-space structure from } E$$$

Lean4

noncomputable instance [NormedField 𝕜] [NormedSpace 𝕜 E] [Star 𝕜] [TrivialStar 𝕜] [StarModule 𝕜 E] :
    NormedSpace 𝕜 (selfAdjoint E) where norm_smul_le _ _ := norm_smul_le _ (_ : E)

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