normedGroup — Mathlib

English

The seminormedGroup structure on a subgroup s equals the induced structure via the subtype map.

Русский

Структура семинормированной группы на подгруппе s равна индуцированной через отображение подтипа.

LaTeX

$$Eq (SubgroupClass.seminormedGroup s) (SeminormedGroup.induced (Subtype ...) E (SubgroupClass.subtype s))$$

Lean4

@[to_additive]
instance (priority := 75) normedGroup [NormedGroup E] {S : Type*} [SetLike S E] [SubgroupClass S E] (s : S) :
    NormedGroup s :=
  NormedGroup.induced _ _ (SubgroupClass.subtype s) Subtype.coe_injective

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