English
The product of normed groups, with the sup norm, forms a normed group; the normed structure extends to all algebraic structure in the product as in the standard construction.
Русский
Произведение нормированных групп с помощью суп-нормы образует нормированную группу; нормированная структура распространяется на произведение аналогично стандартной конструктии.
LaTeX
$$$\text{Prod}(E,F)\text{ is a NormedGroup}$ with $\| (x,y) \| = \max(\|x\|, \|y\|)$$$
Lean4
/-- Finite product of seminormed groups, using the sup norm. -/
@[to_additive /-- Finite product of seminormed groups, using the sup norm. -/
]
instance seminormedGroup : SeminormedGroup (∀ i, G i)
where
norm f := ↑(Finset.univ.sup fun b => ‖f b‖₊)
dist_eq x
y :=
congr_arg (toReal : ℝ≥0 → ℝ) <|
congr_arg (Finset.sup Finset.univ) <|
funext fun a => show nndist (x a) (y a) = ‖x a / y a‖₊ from nndist_eq_nnnorm_div (x a) (y a)
