toNorm — Mathlib

English

In the product of normed spaces E × F with the sup-norm, the norm of a pair is the maximum of the norms of the components: ‖(x,y)‖ = max(‖x‖, ‖y‖).

Русский

В произведении нормированных пространств E × F с максимальной нормой (sup-норма) норма пары равна максимуму норм её составляющих: ‖(x,y)‖ = max(‖x‖, ‖y‖).

LaTeX

$$$\|(x,y)\| = \max \|x\| \|y\|$$$

Lean4

instance toNorm : Norm (E × F) where norm x := ‖x.1‖ ⊔ ‖x.2‖

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