English
Let (E_i) be a family of normed spaces over a field k, and let f_i: E_i → L[k](E_i, E'_i) be a family of continuous linear maps. Then the induced linear map on the tensor product satisfies that its underlying linear map is the tensor of the individual linear maps: (mapL f).toLinearMap = map (i ↦ (f_i).toLinearMap).
Русский
Пусть семейство евклидовых нормированных пространств E_i над полем k и семейство непрерывных линейных отображений f_i: E_i → E'_i. Тогда индуцированное отображение на тензорном произведении удовлетворяет: (mapL f).toLinearMap = map (i ↦ (f_i).toLinearMap).
LaTeX
$$$ (\\mathrm{mapL} f).toLinearMap = \\mathrm{map} \\bigl( \\lambda i, (f i).toLinearMap \\bigr) $$$
Lean4
@[simp]
theorem mapL_coe : (mapL f).toLinearMap = map (fun i ↦ (f i).toLinearMap) :=
by
ext
simp only [mapL, LinearMap.compMultilinearMap_apply, ContinuousLinearMap.coe_coe, liftIsometry_apply_apply,
lift.tprod, ContinuousMultilinearMap.coe_coe, ContinuousMultilinearMap.compContinuousLinearMap_apply, tprodL_toFun,
map_tprod]
