normedGroup — Mathlib

English

The product of normed groups E × F is a normed group with the sup-norm; its structure is defined via a standard construction preserving the normed group axioms.

Русский

Произведение нормированных групп является нормированной группой с суп-нормой; конструкция сохраняет аксиомы нормированной группы.

LaTeX

$$$\text{NormedGroup}(E × F)\;\text{with } \| (x,y) \| = \max(\|x\|,\|y\|)$$$

Lean4

/-- Product of normed groups, using the sup norm. -/
@[to_additive /-- Product of normed groups, using the sup norm. -/
    ]
instance normedGroup [NormedGroup E] [NormedGroup F] : NormedGroup (E × F) :=
  { Prod.seminormedGroup with eq_of_dist_eq_zero := eq_of_dist_eq_zero }

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