English
Product of seminormed groups uses the sup norm and defines the distance via the sup of component distances; i.e., dist((x1,x2),(y1,y2)) = sup{dist_E(x1,y1), dist_F(x2,y2)} with the norm given by the sup of the component norms.
Русский
Произведение полумонормированных групп образует полумонормированную группу, где расстояние равно максимуму расстояний компонентов, а норма — максимум норм компонентов.
LaTeX
$$$\| (x,y) \| = \max(\|x\|, \|y\|)$ и $\mathrm{dist}((x_1,x_2),(y_1,y_2)) = \max(\mathrm{dist}(x_1,y_1),\mathrm{dist}(x_2,y_2))$$$
Lean4
/-- Product of seminormed groups, using the sup norm. -/
@[to_additive /-- Product of seminormed groups, using the sup norm. -/
]
instance seminormedGroup : SeminormedGroup (E × F) where
dist_eq x y := by simp only [Prod.norm_def, Prod.dist_eq, dist_eq_norm_div, Prod.fst_div, Prod.snd_div]
