English
Let f be a family of continuous multilinear maps indexed by ι'. Consider the product map π f which collects those maps into a single multilinear map with target the product space of the E'i. The nonnegative-norm (nnnorm) of π f equals the nonnegative-norm of f. In particular, the process of forming the product map preserves the NN-norm.
Русский
Пусть f — семейство непрерывных многочточельных отображений, индексируемое ι'. Пусть π f обозначает операция сборки этих отображений в одно отображение, величины которого целые на произведение E'i. Тогда NN-норма отображения π f совпадает с NN-нормой f.
LaTeX
$$$\|\pi f\|_{\mathrm{nn}} = \|f\|_{\mathrm{nn}}$$$
Lean4
theorem opNNNorm_pi [∀ i', SeminormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')]
(f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖₊ = ‖f‖₊ :=
eq_of_forall_ge_iff fun _ ↦ by simpa [opNNNorm_le_iff, pi_nnnorm_le_iff] using forall_swap
