normSeminorm — Mathlib

English

The norm on a normed additive group induces a seminorm on the same space by the rule p(x) = ||x||, extending to scalars by the given norm.

Русский

Норма на нормированной аддитивной группе порождает семинорму на том же пространстве через p(x) = ||x||, с сохранением скалярного умножения.

LaTeX

$$$\text{normSeminorm}:= \{\}\text{normAddGroupSeminorm}(E)\,\text{with } \text{smul}' = \text{norm}_s m u l.$$

Lean4

/-- The norm of a seminormed group as a seminorm. -/
def normSeminorm : Seminorm 𝕜 E :=
  { normAddGroupSeminorm E with smul' := norm_smul }

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