seminormedCommGroup — Mathlib

English

A subgroup s of a seminormed group E inherits a seminormed group structure via the restricted norm.

Русский

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

LaTeX

$$$\\text{Subgroup } s \\text{ is a } \\operatorname{SeminormedGroup} \\text{ with norm induced from } E.$$$

Lean4

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

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