seminormedGroup — Mathlib

English

For x ∈ s in a subgroup class S, the norm in s equals the norm in E: ‖x‖ = ‖(x:E)‖.

Русский

Для x ∈ s в классе подгрупп S норма в s равна норме в E: ‖x‖ = ‖(x:E)‖.

LaTeX

$$$ ‖x‖ = ‖(x : E)‖ $$$

Lean4

/-- A subgroup of a seminormed group is also a seminormed group,
with the restriction of the norm. -/
@[to_additive /-- A subgroup of a seminormed additive group is also a seminormed additive group,
    with the restriction of the norm. -/
    ]
instance (priority := 75) seminormedGroup : SeminormedGroup s :=
  SeminormedGroup.induced _ _ (SubgroupClass.subtype s)

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