English
The Cartesian product of two bounded multilinear maps is again a bounded linear map; i.e., the map p ↦ p.fst.prod p.snd is bounded and linear.
Русский
Декартово произведение двух ограниченных мультилинейных отображений снова образует ограниченное линейное отображение; тождественный отображение $p\mapsto p_1\,\mathrm{prod}\, p_2$ ограничено и линейно.
LaTeX
$$$\IsBoundedLinearMap\ 𝕜\ (p \mapsto p.\mathrm fst .prod p.\mathrm snd)$$$
Lean4
/-- Taking the Cartesian product of two continuous multilinear maps is a bounded linear
operation. -/
theorem isBoundedLinearMap_prod_multilinear {E : ι → Type*} [∀ i, SeminormedAddCommGroup (E i)]
[∀ i, NormedSpace 𝕜 (E i)] :
IsBoundedLinearMap 𝕜 fun p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G => p.1.prod p.2 :=
(ContinuousMultilinearMap.prodL 𝕜 E F G).toContinuousLinearEquiv |>.toContinuousLinearMap.isBoundedLinearMap
