seminormedAddCommGroup — Mathlib

English

A submodule s of a normed module E carries a seminormedAddCommGroup structure by restriction of the norm.

Русский

Подмодуль s модуля-нормы E несет структуру семинормированной аддитивной группы за счёт ограничения нормы.

LaTeX

$$$\\text{Submodule } s \\text{ inherits } \\operatorname{SeminormedAddCommGroup}(s)$$$

Lean4

/-- A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.
-/
instance seminormedAddCommGroup [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) :
    SeminormedAddCommGroup s :=
  SeminormedAddCommGroup.induced _ _ s.subtype.toAddMonoidHom

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